Myrto Arapinis, Vincent Cheval, and Stéphanie Delaune. Verifying privacy-type properties in a modular way. In Proceedings of the 25th IEEE Computer Security Foundations Symposium (CSF'12), pp. 95–109, IEEE Computer Society Press, Cambridge Massachusetts, USA, June 2012.
Formal methods have proved their usefulness for analysing the security of protocols. In this setting, privacy-type security properties (e.g. vote-privacy, anonymity, unlinkability) that play an important role in many modern applications are formalised using a notion of equivalence.
In this paper, we study the notion of trace equivalence and we show how to establish such an equivalence relation in a modular way. It is well-known that composition works well when the processes do not share secrets. However, there is no result allowing us to compose processes that rely on some shared secrets such as long term keys. We show that composition works even when the processes share secrets provided that they satisfy some reasonable conditions. Our composition result allows us to prove various equivalence-based properties in a modular way, and works in a quite general setting. In particular, we consider arbitrary cryptographic primitives and processes that use non-trivial else branches.
As an example, we consider the ICAO e-passport standard, and we show how the privacy guarantees of the whole application can be derived from the privacy guarantees of its sub-protocols.
@inproceedings{ACD-csf12,
abstract = {Formal methods have proved their usefulness for
analysing the security of protocols. In this setting,
privacy-type security properties (e.g. vote-privacy,
anonymity, unlinkability) that play an important role
in many modern applications are formalised using a
notion of equivalence.\par In this paper, we study
the notion of trace equivalence and we show how to
establish such an equivalence relation in a modular
way. It is well-known that composition works well
when the processes do not share secrets. However,
there is no result allowing us to compose processes
that rely on some shared secrets such as long term
keys. We show that composition works even when the
processes share secrets provided that they satisfy
some reasonable conditions. Our composition result
allows us to prove various equivalence-based
properties in a modular way, and works in a quite
general setting. In particular, we consider arbitrary
cryptographic primitives and processes that use
non-trivial else branches.\par As an example, we
consider the ICAO e-passport standard, and we show
how the privacy guarantees of the whole application
can be derived from the privacy guarantees of its
sub-protocols.},
address = {Cambridge Massachusetts, USA},
author = {Arapinis, Myrto and Cheval, Vincent and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 25th {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'12)},
OPTDOI = {10.1109/CSF.2012.16},
month = jun,
pages = {95-109},
publisher = {{IEEE} Computer Society Press},
title = {Verifying privacy-type properties in a modular way},
year = {2012},
acronym = {{CSF}'12},
nmonth = {6},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2012-03.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}