From Security Protocols to Pushdown Automata

  • Rémy Chrétien
  • Véronique Cortier
  • Stéphanie Delaune
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7966)


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.


Security Protocol Decidability Result Output Term Unbounded Number Reachability Property 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107–121. IEEE Computer Society Press (2010)Google Scholar
  2. 2.
    Basin, D., Mödersheim, S., Viganò, L.: A symbolic model checker for security protocols. Journal of Information Security 4(3), 181–208 (2005)CrossRefGoogle Scholar
  3. 3.
    Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: 12th ACM Conference on Computer and Communications Security (CCS 2005). ACM Press (2005)Google Scholar
  4. 4.
    Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th Computer Security Foundations Workshop (CSFW 2001). IEEE Computer Society Press (2001)Google Scholar
  5. 5.
    Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. In: 20th Symposium on Logic in Computer Science (2005)Google Scholar
  6. 6.
    Bruso, M., Chatzikokolakis, K., den Hartog, J.: Formal verification of privacy for RFID systems. In: 23rd Computer Security Foundations Symposium, CSF 2010 (2010)Google Scholar
  7. 7.
    Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: 18th ACM Conference on Computer and Communications Security (CCS 2011). ACM Press (2011)Google Scholar
  8. 8.
    Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. J. Autom. Reasoning 48(2), 263–292 (2012)MathSciNetzbMATHCrossRefGoogle Scholar
  9. 9.
    Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 148–164. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  10. 10.
    Cortier, V., Delaune, S.: A method for proving observational equivalence. In: 22nd IEEE Computer Security Foundations Symposium (CSF 2009). IEEE Computer Society Press (2009)Google Scholar
  11. 11.
    Cremers, C.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement. In: 15th ACM Conference on Computer and Communications Security (CCS 2008). ACM (2008)Google Scholar
  12. 12.
    Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci. 1(4), 297–316 (1976)zbMATHCrossRefGoogle Scholar
  13. 13.
    Rusinowitch, M., Turuani, M.: Protocol Insecurity with Finite Number of Sessions and Composed Keys is NP-complete. Theoretical Computer Science 299, 451–475 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  14. 14.
    Sénizergues, G.: The equivalence problem for deterministic pushdown automata is decidable. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol. 1256, pp. 671–681. Springer, Heidelberg (1997)Google Scholar
  15. 15.
    Sénizergues, G.: L(A)=L(B)? Decidability results from complete formal systems. Theor. Comput. Sci. 251(1-2), 1–166 (2001)zbMATHCrossRefGoogle Scholar
  16. 16.
    Stirling, C.: Deciding DPDA equivalence is primitive recursive. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, pp. 821–832. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  17. 17.
    Tiu, A., Dawson, J.E.: Automating open bisimulation checking for the SPI calculus. In: 23rd IEEE Computer Security Foundations Symposium (CSF 2010), pp. 307–321 (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Rémy Chrétien
    • 1
    • 2
  • Véronique Cortier
    • 1
  • Stéphanie Delaune
    • 2
  1. 1.CNRSLORIAFrance
  2. 2.LSV, ENS Cachan & CNRS & INRIA Saclay Île-deFrance

Personalised recommendations