Véronique Cortier and Stéphanie Delaune. A method for proving observational equivalence. In Proceedings of the 22nd IEEE Computer Security Foundations Symposium (CSF'09), pp. 266–276, IEEE Computer Society Press, Port Jefferson, New York, USA, July 2009.
Formal methods have proved their usefulness for analyzing the security of protocols. Most existing results focus on trace properties like secrecy or authentication. There are however several security properties, which cannot be defined (or cannot be naturally defined) as trace properties and require the notion of observational equivalence. Typical examples are anonymity, privacy related properties or statements closer to security properties used in cryptography.
In this paper, we consider the applied pi calculus and we show that for determinate processes, observational equivalence actually coincides with trace equivalence, a notion simpler to reason with. We exhibit a large class of determinate processes, called simple processes, that capture most existing protocols and cryptographic primitives. Then, for simple processes without replication, we reduce the decidability of trace equivalence to deciding an equivalence relation introduced by M. Baudet. Altogether, this yields the first decidability result of observational equivalence for a general class of equational theories.
@inproceedings{CD-csf09,
abstract = {Formal methods have proved their usefulness for
analyzing the security of protocols. Most existing
results focus on trace properties like secrecy or
authentication. There are however several security
properties, which cannot be defined (or cannot be
naturally defined) as trace properties and require
the notion of \emph{observational equivalence}.
Typical examples are anonymity, privacy related
properties or statements closer to security
properties used in cryptography.\par In this paper,
we consider the applied pi calculus and we show that
for \emph{determinate} processes, observational
equivalence actually coincides with trace
equivalence, a notion simpler to reason with.
We~exhibit a large class of determinate processes,
called \emph{simple processes}, that capture most
existing protocols and cryptographic primitives.
Then, for simple processes without replication,
we~reduce the decidability of trace equivalence to
deciding an equivalence relation introduced by
M.~Baudet. Altogether, this yields the first
decidability result of observational equivalence for
a general class of equational theories.},
address = {Port Jefferson, New York, USA},
author = {Cortier, V{\'e}ronique and Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 22nd {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'09)},
OPTDOI = {10.1109/CSF.2009.9},
month = jul,
pages = {266-276},
publisher = {{IEEE} Computer Society Press},
title = {A~method for proving observational equivalence},
year = {2009},
acronym = {{CSF}'09},
nmonth = {7},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2009-04.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}