Skip to main content
Kent Academic Repository

Composing security protocols: from confidentiality to privacy

Arapinis, Myrto and Cheval, Vincent and Delaune, Stéphanie (2015) Composing security protocols: from confidentiality to privacy. In: Focardi, Ricardo and Myers, Andrew, eds. Principles of Security and Trust 4th International Conference. Lecture Notes in Computer Science . Springer, Berlin, Germany, pp. 324-343. ISBN 978-3-662-46665-0. E-ISBN 978-3-662-46666-7. (doi:10.1007/978-3-662-46666-7_17) (Access to this publication is currently restricted. You may be able to access a copy if URLs are provided) (KAR id:46880)

PDF Publisher pdf
Language: English

Restricted to Repository staff only
[thumbnail of ACD-post15.pdf]
PDF (Long version of the paper) Supplemental Material
Language: English

Restricted to Repository staff only
[thumbnail of Long version of the paper]
Official URL:


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 derive some security properties on a protocol from the security analysis performed on each of its sub-protocols 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) expressed using a notion of equivalence. We illustrate the usefulness of our composition results on protocols from the 3G phone application and electronic passport.

Item Type: Book section
DOI/Identification number: 10.1007/978-3-662-46666-7_17
Additional information: To appear
Uncontrolled keywords: Cryptographic protocols, Formal verification, Symbolic model, Composition, Equivalence properties, Reachability properties
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Q Science > QA Mathematics (inc Computing science) > QA 9 Formal systems, logics
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 12:00 UTC
Last Modified: 17 Aug 2022 10:58 UTC
Resource URI: (The current URI for this page, for reference purposes)

University of Kent Author Information

Cheval, Vincent.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.