Skip to main content

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)

PDF - Publisher pdf
Restricted to Repository staff only
Contact us about this Publication Download (318kB)
[img]
PDF (Long version of the paper) - Supplemental Material
Restricted to Repository staff only
Contact us about this Publication Download (734kB)
[img]
Official URL
http://dx.doi.org/10.1007/978-3-662-46666-7_17

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 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: Faculties > Sciences > School of Computing > Security Group
Depositing User: Vincent Cheval
Date Deposited: 23 Jan 2015 12:00 UTC
Last Modified: 15 Oct 2019 15:06 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/46880 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year