From security protocols to pushdown automata

From security protocols to pushdown automata. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. ACM Transactions on Computational Logic, 17(3), November 2015.

Download

[PDF] [HTML]

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.
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. We further show that checking for equivalence of protocols is actually equivalent to checking for equivalence of generalized, real-time deterministic pushdown automata.
Very recently, the algorithm for checking for equivalence of deterministic pushdown automata has been implemented. We have implemented our translation from protocols to pushdown automata, yielding the first tool that decides equivalence of (some class of) protocols, for an unbounded number of sessions. As an application, we have analyzed some protocols of the literature including a simplified version of the basic access control (BAC) protocol used in biometric passports.

BibTeX

@Article{Tocl2015,
  author = 	 {R\'emy Chr\'etien and V\'eronique Cortier and St\'ephanie Delaune},
  title = 	 {From security protocols to
  pushdown automata},
  journal = 	 {ACM Transactions on Computational Logic},
  year = 	 {2015},
  OPTkey = 	 {},
  volume = 	 {17},
  number = 	 {3},
  OPTpages = 	 {},
  month = 	 {November},
  doi = {10.1145/2811262},
  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.
We further show that checking for equivalence of protocols is actually equivalent to checking for equivalence of generalized, real-time deterministic
pushdown automata.
\par
Very recently, the algorithm for checking for equivalence of
  deterministic pushdown automata has been implemented. We have
  implemented our translation from protocols to pushdown automata,
  yielding the first tool that decides equivalence of 
(some class of) protocols, for an unbounded number of sessions. 
As an application, we have analyzed some
protocols of the
literature 
including a simplified version of the basic access control (BAC) protocol used in biometric passports.},
}