Composing security protocols: from confidentiality to privacy
Myrto Arapinis, Vincent Cheval, and St\'ephanie Delaune

TL;DR
This paper develops formal methods for safely composing security protocols, enabling the derivation of security and privacy properties from individual sub-protocol analyses, with applications to real-world systems.
Contribution
It introduces new composition results for security protocols modeled with an equational theory and process algebra, extending analysis to privacy properties like anonymity and unlinkability.
Findings
Composition results enable security property derivation from sub-protocols
Applicable to confidentiality and privacy properties
Validated on 3G phone and electronic passport protocols
Abstract
Security protocols are used in many of our daily-life applications, and our privacy largely depends on their design. Formal verification techniques have proved their usefulness to analyse these protocols, but they become so complex that modular techniques have to be developed. We propose several results to safely compose security protocols. We consider arbitrary primitives modeled using an equational theory, and a rich process algebra close to the applied pi calculus. Relying on these composition results, we are able to derive some security properties on a protocol from the security analysis performed on each sub-protocol individually. We consider parallel composition and the case of key-exchange protocols. Our results apply to deal with confidentiality but also privacy-type properties (e.g. anonymity, unlinkability) expressed using a notion of equivalence. We illustrate the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Authentication Protocols Security · User Authentication and Security Systems · Access Control and Trust
