Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Typing messages for free in security protocols: the case of equivalence properties. In Proceedings of the 25th International Conference on Concurrency Theory (CONCUR'14), pp. 372–386, Lecture Notes in Computer Science 8704, Springer, Rome, Italy, September 2014.
Privacy properties such as untraceability, vote secrecy, or anonymity are typically expressed as behavioural equivalence in a process algebra that models security protocols. In this paper, we study how to decide one particular relation, namely trace equivalence, for an unbounded number of sessions.
Our first main contribution is to reduce the search space for attacks. Specifically, we show that if there is an attack then there is one that is well-typed. Our result holds for a large class of typing systems and a large class of determinate security protocols. Assuming finitely many nonces and keys, we can derive from this result that trace equivalence is decidable for an unbounded number of sessions for a class of tagged protocols, yielding one of the first decidability results for the unbounded case. As an intermediate result, we also provide a novel decision procedure in the case of a bounded number of sessions.
@inproceedings{CCD-concur14,
abstract = {Privacy properties such as untraceability, vote
secrecy, or anonymity are typically expressed as
behavioural equivalence in a process algebra that
models security protocols. In this paper, we study
how to decide one particular relation, namely trace
equivalence, for an unbounded number of sessions.\par
Our first main contribution is to reduce the search
space for attacks. Specifically, we show that if
there is an attack then there is one that is
well-typed. Our result holds for a large class of
typing systems and a large class of determinate
security protocols. Assuming finitely many nonces and
keys, we can derive from this result that trace
equivalence is decidable for an unbounded number of
sessions for a class of tagged protocols, yielding
one of the first decidability results for the
unbounded case. As an intermediate result, we also
provide a novel decision procedure in the case of a
bounded number of sessions.},
address = {Rome, Italy},
author = {Chr{\'e}tien, R{\'e}my and Cortier, V{\'e}ronique and
Delaune, St{\'e}phanie},
booktitle = {{P}roceedings of the 25th {I}nternational
{C}onference on {C}oncurrency {T}heory ({CONCUR}'14)},
OPTDOI = {10.1007/978-3-662-44584-6_26},
editor = {Baldan, Paolo and Gorla, Daniele},
month = sep,
pages = {372-386},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
title = {Typing messages for free in security protocols:
the~case of equivalence properties},
volume = {8704},
year = {2014},
acceptrate = {35/124},
acronym = {{CONCUR}'14},
nmonth = {9},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/
CCD-concur14-long.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}