Document Open Access Logo

Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions

Authors Emanuele D'Osualdo , Felix Stutz

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.31.pdf
  • Filesize: 0.64 MB
  • 23 pages

Document Identifiers

Author Details

Emanuele D'Osualdo
  • Imperial College London, UK
Felix Stutz
  • Max Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany
  • Saarland University, Saarland Informatics Campus, Saarbrücken, Germany

Funding

  • D'Osualdo, Emanuele: EU Horizon 2020 Marie Curie Individual Fellowship.
  • Stutz, Felix: supported by Imperial College London and International Max Planck Research School for Computer Science.

Acknowledgements

We would like to thank Alwen Tiu, Roland Meyer and Véronique Cortier for the useful feedback.

Cite As Get BibTex

Emanuele D'Osualdo and Felix Stutz. Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 31:1-31:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CONCUR.2020.31

Abstract

We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied πcalc, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness. We provide a prototype implementation and we report on its performance on some textbook examples.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
Keywords
  • Security Protocols
  • Infinite-State Verification
  • Ideal Completions for WSTS

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Martín Abadi and Véronique Cortier. Deciding knowledge in security protocols under (many more) equational theories. In CSFW, pages 62-76. IEEE Computer Society, 2005. Google Scholar
  2. Myrto Arapinis and Marie Duflot. Bounding messages for free in security protocols - extension to various security properties. Inf. Comput., 239:182-215, 2014. Google Scholar
  3. Alessandro Armando, David A. Basin, Yohan Boichut, Yannick Chevalier, Luca Compagna, Jorge Cuéllar, Paul Hankes Drielsma, Pierre-Cyrille Héam, Olga Kouchnarenko, Jacopo Mantovani, Sebastian Mödersheim, David von Oheimb, Michaël Rusinowitch, Judson Santiago, Mathieu Turuani, Luca Viganò, and Laurent Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In CAV, volume 3576 of Lecture Notes in Computer Science, pages 281-285. Springer, 2005. Google Scholar
  4. Bruno Blanchet. Modeling and verifying security protocols with the applied pi calculus and proverif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, 2016. Google Scholar
  5. Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program., 75(1):3-51, 2008. URL: https://doi.org/10.1016/j.jlap.2007.06.002.
  6. Bruno Blanchet and Andreas Podelski. Verification of cryptographic protocols: tagging enforces termination. Theor. Comput. Sci., 333(1-2):67-90, 2005. Google Scholar
  7. Michael Blondin, Alain Finkel, Christoph Haase, and Serge Haddad. Approaching the coverability problem continuously. In TACAS, volume 9636 of Lecture Notes in Computer Science, pages 480-496. Springer, 2016. Google Scholar
  8. Michael Blondin, Alain Finkel, and Pierre McKenzie. Handling infinitely branching well-structured transition systems. Inf. Comput., 258:28-49, 2018. Google Scholar
  9. Michael Burrows, Martín Abadi, and Roger M. Needham. A logic of authentication. In SOSP'89, pages 1-13. ACM, 1989. Google Scholar
  10. Rohit Chadha, Vincent Cheval, Ştefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. ACM Trans. Comput. Log., 17(4):23:1-23:32, 2016. Google Scholar
  11. Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. DEEPSEC: deciding equivalence properties in security protocols theory and practice. In IEEE Symposium on Security and Privacy, pages 529-546. IEEE Computer Society, 2018. Google Scholar
  12. Yannick Chevalier, Ralf Küsters, Michaël Rusinowitch, and Mathieu Turuani. An NP decision procedure for protocol insecurity with XOR. In LICS, pages 261-270. IEEE Computer Society, 2003. Google Scholar
  13. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Typing messages for free in security protocols: The case of equivalence properties. In CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 372-386. Springer, 2014. Google Scholar
  14. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. In CSF'15, pages 170-184. IEEE Computer Society, 2015. Google Scholar
  15. Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. A type system for privacy properties. In ACM Conference on Computer and Communications Security, pages 409-423. ACM, 2017. Google Scholar
  16. Morten Dahl, Naoki Kobayashi, Yunde Sun, and Hans Hüttel. Type-based automated verification of authenticity in asymmetric cryptographic protocols. In ATVA, volume 6996 of Lecture Notes in Computer Science, pages 75-89. Springer, 2011. Google Scholar
  17. Danny Dolev and Andrew Chi-Chih Yao. On the security of public key protocols. IEEE Trans. Information Theory, 29(2):198-207, 1983. Google Scholar
  18. Emanuele D'Osualdo, Luke Ong, and Alwen Tiu. Deciding secrecy of security protocols for an unbounded number of sessions: The case of depth-bounded processes. In CSF, pages 464-480. IEEE Computer Society, 2017. Google Scholar
  19. Emanuele D'Osualdo and Felix Stutz. Decidable inductive invariants for verification of cryptographic protocols with unbounded sessions. CoRR, abs/1911.05430, 2019. URL: http://arxiv.org/abs/1911.05430.
  20. Emanuele D'Osualdo and Felix Stutz. Lemma9, version 1.0, 2020. URL: https://doi.org/10.5281/zenodo.3950846.
  21. Nancy A. Durgin, Patrick D. Lincoln, John C. Mitchell, and Andre Scedrov. Undecidability of bounded security protocols. In Workshop on Formal Methods and Security Protocols, 1999. Google Scholar
  22. Alain Finkel and Jean Goubault-Larrecq. Forward analysis for WSTS, part I: completions. In STACS, volume 3 of LIPIcs, pages 433-444, 2009. Google Scholar
  23. Sibylle B. Fröschle. Leakiness is decidable for well-founded protocols. In POST'15, pages 176-195, 2015. Google Scholar
  24. Reiner Hüchting, Rupak Majumdar, and Roland Meyer. Bounds on mobility. In CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 357-371. Springer, 2014. Google Scholar
  25. Gavin Lowe. Some new attacks upon security protocols. In Ninth IEEE Computer Security Foundations Workshop, March 10 - 12, 1996, Dromquinna Manor, Kenmare, County Kerry, Ireland, pages 162-169. IEEE Computer Society, 1996. Google Scholar
  26. Simon Meier, Benedikt Schmidt, Cas Cremers, and David A. Basin. The TAMARIN prover for the symbolic analysis of security protocols. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 696-701. Springer, 2013. Google Scholar
  27. Roland Meyer. On boundedness in depth in the π-calculus. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and C.-H. Luke Ong, editors, IFIP TCS, volume 273 of IFIP, pages 477-489. Springer, 2008. Google Scholar
  28. Roger M. Needham and Michael D. Schroeder. Using encryption for authentication in large networks of computers. Commun. ACM, 21(12):993-999, 1978. Google Scholar
  29. David J. Otway and Owen Rees. Efficient and timely mutual authentication. Operating Systems Review, 21(1):8-10, 1987. Google Scholar
  30. Lawrence C. Paulson. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 6(1-2):85-128, 1998. Google Scholar
  31. Mark D. Ryan and Ben Smyth. Applied pi-calculus. In Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 112-142. IOS Press, 2011. Google Scholar
  32. Benedikt Schmidt, Simon Meier, Cas J. F. Cremers, and David A. Basin. Automated analysis of Diffie-Hellman protocols and advanced security properties. In CSF, pages 78-94. IEEE Computer Society, 2012. Google Scholar
  33. Felix Stutz. Decidable inductive invariants for verification of cryptographic protocols with unbounded sessions. Master’s thesis, Saarland University, 2019. Google Scholar
  34. Alwen Tiu, Rajeev Goré, and Jeremy E. Dawson. A proof theoretic analysis of intruder theories. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  35. Alwen Tiu, Nam Nguyen, and Ross Horne. SPEC: an equivalence checker for security protocols. In APLAS, volume 10017 of Lecture Notes in Computer Science, pages 87-95, 2016. Google Scholar
  36. Thomas Wies, Damien Zufferey, and Thomas A. Henzinger. Forward analysis of depth-bounded processes. In FoSSaCS, volume 6014 of Lecture Notes in Computer Science, pages 94-108. Springer, 2010. Google Scholar
  37. Damien Zufferey, Thomas Wies, and Thomas A. Henzinger. Ideal abstractions for well-structured transition systems. In VMCAI'12', volume 7148 of LNCS, pages 445-460. Springer, 2012. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact