Composing Security Protocols: From Confidentiality to Privacy

Myrto Arapinis; Vincent Cheval; Stéphanie Delaune

doi:10.1007/978-3-662-46666-7_17

Composing Security Protocols: From Confidentiality to Privacy

Myrto Arapinis, Vincent Cheval, Stéphanie Delaune

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Principles of Security and Trust
Subtitle of host publication	4th 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
Publisher	Springer Berlin Heidelberg
Pages	324-343
Number of pages	20
ISBN (Electronic)	978-3-662-46666-7
ISBN (Print)	978-3-662-46665-0
DOIs	https://doi.org/10.1007/978-3-662-46666-7_17
Publication status	Published - 18 Apr 2015
Event	4th International Conference on Principles of Security and Trust - London, United Kingdom Duration: 11 Apr 2015 → 18 Apr 2015 https://etaps.org/2015/post

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin Heidelberg
Volume	9036
ISSN (Print)	0302-9743

Conference

Conference	4th International Conference on Principles of Security and Trust
Abbreviated title	POST 2015
Country/Territory	United Kingdom
City	London
Period	11/04/15 → 18/04/15
Internet address	https://etaps.org/2015/post

Access to Document

10.1007/978-3-662-46666-7_17

Arapinis et al 2014 Composing security protocolsAccepted author manuscript, 432 KB

http://link.springer.com/chapter/10.1007%2F978-3-662-46666-7_17

Myrto Arapinis
- marapiniinf.ed.acuk
Person: Academic: Research Active

Cite this

Arapinis, M., Cheval, V., & Delaune, S. (2015). Composing Security Protocols: From Confidentiality to Privacy. In Principles of Security and Trust: 4th 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 (pp. 324-343). (Lecture Notes in Computer Science; Vol. 9036). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-46666-7_17

Arapinis, Myrto ; Cheval, Vincent ; Delaune, Stéphanie. / Composing Security Protocols: From Confidentiality to Privacy. Principles of Security and Trust: 4th 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. Springer Berlin Heidelberg, 2015. pp. 324-343 (Lecture Notes in Computer Science).

@inproceedings{19e6c6a370624b028af7f9e52cd48a73,

title = "Composing Security Protocols: From Confidentiality to Privacy",

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.",

author = "Myrto Arapinis and Vincent Cheval and St{\'e}phanie Delaune",

year = "2015",

month = apr,

day = "18",

doi = "10.1007/978-3-662-46666-7_17",

language = "English",

isbn = "978-3-662-46665-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "324--343",

booktitle = "Principles of Security and Trust",

note = "4th International Conference on Principles of Security and Trust, POST 2015 ; Conference date: 11-04-2015 Through 18-04-2015",

url = "https://etaps.org/2015/post",

}

Arapinis, M, Cheval, V & Delaune, S 2015, Composing Security Protocols: From Confidentiality to Privacy. in Principles of Security and Trust: 4th 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. Lecture Notes in Computer Science, vol. 9036, Springer Berlin Heidelberg, pp. 324-343, 4th International Conference on Principles of Security and Trust, London, United Kingdom, 11/04/15. https://doi.org/10.1007/978-3-662-46666-7_17

Composing Security Protocols: From Confidentiality to Privacy. / Arapinis, Myrto; Cheval, Vincent; Delaune, Stéphanie.

Principles of Security and Trust: 4th 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. Springer Berlin Heidelberg, 2015. p. 324-343 (Lecture Notes in Computer Science; Vol. 9036).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Composing Security Protocols: From Confidentiality to Privacy

AU - Arapinis, Myrto

AU - Cheval, Vincent

AU - Delaune, Stéphanie

PY - 2015/4/18

Y1 - 2015/4/18

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-662-46666-7_17

DO - 10.1007/978-3-662-46666-7_17

M3 - Conference contribution

SN - 978-3-662-46665-0

T3 - Lecture Notes in Computer Science

SP - 324

EP - 343

BT - Principles of Security and Trust

PB - Springer Berlin Heidelberg

T2 - 4th International Conference on Principles of Security and Trust

Y2 - 11 April 2015 through 18 April 2015

ER -

Arapinis M, Cheval V, Delaune S. Composing Security Protocols: From Confidentiality to Privacy. In Principles of Security and Trust: 4th 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. Springer Berlin Heidelberg. 2015. p. 324-343. (Lecture Notes in Computer Science). doi: 10.1007/978-3-662-46666-7_17

Composing Security Protocols: From Confidentiality to Privacy

Abstract

Publication series

Conference

Access to Document

Fingerprint

Profiles

Myrto Arapinis

Cite this