Myrto Arapinis, Vincent Cheval, and Stéphanie Delaune. Composing security protocols: from confidentiality to privacy. In Proceedings of the 4th International Conference on Principles of Security and Trust (POST'15), pp. 324–343, Lecture Notes in Computer Science 9036, Springer, London, UK, April 2015.
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.
@inproceedings{ACD-post15,
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.\par 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.},
address = {London, UK},
author = {Arapinis, Myrto and Cheval, Vincent and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 4th {I}nternational {C}onference
on {P}rinciples of {S}ecurity and {T}rust
({POST}'15)},
OPTDOI = {10.1007/978-3-662-46666-7_17},
editor = {Focardi, Riccardo and Myers, Andrew},
month = apr,
pages = {324-343},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Composing security protocols: from confidentiality to
privacy},
volume = {9036},
year = {2015},
acceptrate = {17/55},
acronym = {{POST}'15},
nmonth = {4},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}