@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@InProceedings{icalp2013,
  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  
(only symmetric encryption, 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.
},
  author = 	 {R\'emy Chr\'etien and V\'eronique Cortier and  St\'ephanie Delaune},
  title = 	 {From security protocols to pushdown automata},
  booktitle = {{P}roceedings of the 40th {I}nternational
                   {C}olloquium on {A}utomata, {L}anguages and
                   {P}rogramming ({ICALP}'13)},
  pages = 	 {137-149},
  year = 	 {2013},
  OPTeditor = 	 {},
  volume = 	 {7966},
  OPTnumber = 	 {},
  series = 	 {Lecture Notes in Computer Science},
  address = 	 {Riga, Lituania},
  month = 	 {July},
  OPTorganization = {},
  publisher = {Springer},
  DOI = {10.1007/978-3-642-39212-2_15},
}