Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. From security protocols to pushdown automata. In Proceedings of the 40th International Colloquium on Automata, Languages and Programming (ICALP'13) -- Part II, pp. 137–149, Lecture Notes in Computer Science 7966, Springer, Riga, Latvia, July 2013.
Formal methods have been very successful in analyzing security protocols for reachability properties such as secrecy or authentication. In contrast, there are very few results for equivalence-based properties, crucial for studying e.g. privacy-like properties such as anonymity or vote secrecy.
We study the problem of checking equivalence of security protocols for an unbounded number of sessions. Since replication leads very quickly to undecidability (even in the simple case of secrecy), we focus on a limited fragment of protocols (standard primitives but pairs, one variable per protocol's rules) for which the secrecy preservation problem is known to be decidable. Surprisingly, this fragment turns out to be undecidable for equivalence. Then, restricting our attention to deterministic protocols, we propose the first decidability result for checking equivalence of protocols for an unbounded number of sessions. This result is obtained through a characterization of equivalence of protocols in terms of equality of languages of (generalized, real-time) deterministic pushdown automata.
@inproceedings{CCD-icalp13,
abstract = {Formal methods have been very successful in analyzing
security protocols for reachability properties such
as secrecy or authentication. In contrast, there are
very few results for equivalence-based properties,
crucial for studying e.g. privacy-like properties
such as anonymity or vote secrecy.\par We study the
problem of checking equivalence of security protocols
for an unbounded number of sessions. Since
replication leads very quickly to undecidability
(even in the simple case of secrecy), we focus on a
limited fragment of protocols (standard primitives
but pairs, one variable per protocol's rules) for
which the secrecy preservation problem is known to be
decidable. Surprisingly, this fragment turns out to
be undecidable for equivalence. Then, restricting our
attention to deterministic protocols, we propose the
first decidability result for checking equivalence of
protocols for an unbounded number of sessions. This
result is obtained through a characterization of
equivalence of protocols in terms of equality of
languages of (generalized, real-time) deterministic
pushdown automata.},
address = {Riga, Latvia},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 40th {I}nternational
{C}olloquium on {A}utomata, {L}anguages and
{P}rogramming ({ICALP}'13)~-- {P}art~{II}},
OPTDOI = {10.1007/978-3-642-39212-2_15},
editor = {Fomin, Fedor V. and Freivalds, R{\=u}si{\c{n}}{\v{s}} and
Kwiatkowska, Marta and Peleg, David},
month = jul,
pages = {137-149},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {From security protocols to pushdown automata},
volume = {7966},
year = {2013},
acronym = {{ICALP}'13},
nmonth = {7},
OPTLONGPDF = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
CCD-icalp13-long.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}