Typing Messages for Free in Security Protocols: The Case of Equivalence Properties

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


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.


Typing System Decision Procedure Security Protocol Decidability Result Equivalence 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.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th Symposium on Principles of Programming Languages (POPL 2001). ACM Press (2001)Google Scholar
  2. 2.
    Abadi, M., Needham, R.M.: Prudent engineering practice for cryptographic protocols. IEEE Trans. Software Eng. 22(1), 6–15 (1996)CrossRefGoogle Scholar
  3. 3.
    Amadio, R.M., Charatonik, W.: On name generation and set-based analysis in the Dolev-Yao model. In: Brim, L., Jančar, P., Křetínský, M., Kučera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 499–514. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  4. 4.
    Arapinis, M., Duflot, M.: Bounding messages for free in security protocols. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 376–387. Springer, Heidelberg (2007)Google Scholar
  5. 5.
    Backes, M., Hritcu, C., Maffei, M.: Automated verification of remote electronic voting protocols in the applied pi-calculus. In: 21st IEEE Computer Security Foundations Symposium (CSF 2008), pp. 195–209. IEEE Computer Society (2008)Google Scholar
  6. 6.
    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
  7. 7.
    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
  8. 8.
    Blanchet, B., Podelski, A.: Verification of cryptographic protocols: Tagging enforces termination. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol. 2620, pp. 136–152. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. 9.
    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
  10. 10.
    Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108–127. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  11. 11.
    Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: Negative tests and non-determinism. In: 18th ACM Conference on Computer and Communications SecurityGoogle Scholar
  12. 12.
    Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoretical Computer Science 492, 1–39 (2013)CrossRefzbMATHMathSciNetGoogle Scholar
  13. 13.
    Chrétien, R., Cortier, V., Delaune, S.: From security protocols to pushdown automata. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 137–149. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  14. 14.
    Chrétien, R., Cortier, V., Delaune, S.: Typing messages for free in security protocols: the case of equivalence properties. Technical Report 8546, Inria (June 2014)Google Scholar
  15. 15.
    Clark, J., Jacob, J.: A survey of authentication protocol literature: Version 1.0 (1997)Google Scholar
  16. 16.
    Comon-Lundh, H., Cortier, V., Zalinescu, E.: Deciding security properties for cryptographic protocols. Application to key cycles. ACM Transactions on Computational Logic (TOCL) 11(4) (2010)Google Scholar
  17. 17.
    Cortier, V., Delaune, S.: Safely composing security protocols. Formal Methods in System Design 34(1), 1–36 (2009)CrossRefzbMATHGoogle Scholar
  18. 18.
    Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, Elsevier (1990)Google Scholar
  19. 19.
    Guttman, J.D., Thayer, F.J.: Protocol independence through disjoint encryption. In: 13th Computer Security Foundations Workshop (CSFW 2000). IEEE Comp. Soc. Press (2000)Google Scholar
  20. 20.
    Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communications Security (2001)Google Scholar
  21. 21.
    Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 363–374. Springer, Heidelberg (2003)Google Scholar
  22. 22.
    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
  23. 23.
    Tiu, A., Goré, R., Dawson, J.E.: A proof theoretic analysis of intruder theories. Logical Methods in Computer Science 6(3) (2010)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2014

Authors and Affiliations

  • Rémy Chrétien
    • 1
    • 2
  • Véronique Cortier
    • 1
  • Stéphanie Delaune
    • 2
  1. 1.LORIA, INRIA Nancy - Grand-EstNancyFrance
  2. 2.LSV, ENS Cachan & CNRSCachanFrance

Personalised recommendations