Decidability of trace equivalence for protocols with nonces

Decidability of trace equivalence for protocols with nonces. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. In Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF'15), IEEE Computer Society Press, July 2015.

Download

[PDF] [HTML]

Abstract

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.

BibTeX

@InProceedings{DecEquiv-CSF15,
  author = 	 {R\'emy Chr\'etien and V\'eronique Cortier and St\'ephanie Delaune},
  title = 	 {Decidability of trace equivalence for protocols with nonces},
  booktitle = {{P}roceedings of the 28th {IEEE} {C}omputer {S}ecurity {F}oundations {S}ymposium ({CSF}'15)}, 
   month = {July}, 
   publisher = {{IEEE} Computer Society Press},
  year = 	 {2015},
  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.},
doi ={10.1109/CSF.2015.19},
}