Composing Security Protocols: From Confidentiality to Privacy

Myrto Arapinis, Vincent Cheval, Stéphanie Delaune

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publicationPrinciples of Security and Trust
Subtitle of host publication4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings
PublisherSpringer Berlin Heidelberg
Number of pages20
ISBN (Electronic)978-3-662-46666-7
ISBN (Print)978-3-662-46665-0
Publication statusPublished - 18 Apr 2015
Event4th International Conference on Principles of Security and Trust - London, United Kingdom
Duration: 11 Apr 201518 Apr 2015

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
ISSN (Print)0302-9743


Conference4th International Conference on Principles of Security and Trust
Abbreviated titlePOST 2015
Country/TerritoryUnited Kingdom
Internet address


Dive into the research topics of 'Composing Security Protocols: From Confidentiality to Privacy'. Together they form a unique fingerprint.

Cite this