Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. In Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF'15), pp. 170–184, IEEE Computer Society Press, Verona, Italy, July 2015.
Privacy properties such as anonymity, unlinkability, or vote secrecy are typically expressed as equivalence properties.
In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonces. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.
@inproceedings{CCD-csf15,
abstract = {Privacy properties such as anonymity, unlinkability,
or vote secrecy are typically expressed as
equivalence properties.\par In this paper, we provide
the first decidability result for trace equivalence
of security protocols, for an unbounded number of
sessions and unlimited fresh nonces. Our class
encompasses most symmetric key protocols of the
literature, in their tagged variant.},
address = {Verona, Italy},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 28th {IEEE} {C}omputer
{S}ecurity {F}oundations {S}ymposium ({CSF}'15)},
OPTDOI = {10.1109/CSF.2015.19},
month = jul,
pages = {170-184},
publisher = {{IEEE} Computer Society Press},
title = {Decidability of trace equivalence for protocols with
nonces},
year = {2015},
acronym = {{CSF}'15},
nmonth = {7},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
CCD-csf15-long.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}