Document Open Access Logo

Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper)

Author Stéphanie Delaune

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.2.pdf
  • Filesize: 0.57 MB
  • 9 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • Security protocols
  • Formal verification

Metrics

Abstract

Cryptographic protocols are essential to secure communication but remain difficult to design correctly, motivating the need for rigorous verification methods. This paper provides a brief overview of symbolic verification techniques, focusing on the evolution and impact of the tool ProVerif over the past 25 years. We discuss its core principles, key extensions for richer security properties, and recent work on handling algebraic theories such as exclusive-or (XOR). We conclude by highlighting ongoing challenges, including usability and interoperability between verification approaches.

Cite As Get BibTex

Stéphanie Delaune. Formal Verification of Security Protocols: 25 Years of ProVerif (Invited Paper). In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 2:1-2:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.2

Author Details

Stéphanie Delaune
  • Univ Rennes, CNRS, IRISA, France

Funding

This work received funding from the France 2030 program managed by the French National Research Agency under grant agreement No. ANR-22-PECY-0006.

References

  1. M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. In 29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2002), pages 33-44, Portland, Oregon, January 2002. ACM Press. Google Scholar
  2. X. Allamigeon and B. Blanchet. Reconstruction of attacks against cryptographic protocols. In 18th IEEE Computer Security Foundations Workshop, (CSFW-18 2005), 20-22 June 2005, Aix-en-Provence, France, pages 140-154. IEEE Computer Society, 2005. URL: https://doi.org/10.1109/CSFW.2005.25.
  3. M. Arapinis. Sécurité des protocoles cryptographiques: décidabilité et résultats de réduction. PhD thesis, École normale supérieure de Cachan, France, 2008. Google Scholar
  4. M. Arapinis, E. Ritter, and M. Dermot Ryan. StatVerif: Verification of stateful processes. In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011, pages 33-47. IEEE Computer Society, 2011. URL: https://doi.org/10.1109/CSF.2011.10.
  5. D. Baelde, A. Debant, and S. Delaune. Proving unlinkability using ProVerif through desynchronised bi-processes. In 36th IEEE Computer Security Foundations Symposium, (CSF'23), Dubrovnik, Croatia, July 10-14, 2023, pages 75-90. IEEE, 2023. URL: https://doi.org/10.1109/CSF57540.2023.00022.
  6. M. Barbosa, G. Barthe, K. Bhargavan, B. Blanchet, C. Cremers, K. Liao, and B. Parno. Sok: Computer-aided cryptography. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, pages 777-795. IEEE, 2021. URL: https://doi.org/10.1109/SP40001.2021.00008.
  7. D. A. Basin, R. Sasse, and J. Toro-Pozo. The EMV standard: Break, Fix, Verify. In 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021, pages 1766-1781. IEEE, 2021. URL: https://doi.org/10.1109/SP40001.2021.00037.
  8. K. Bhargavan, B. Blanchet, and N. Kobeissi. Verified models and reference implementations for the TLS 1.3 standard candidate. In 38th IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017, pages 483-502. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/SP.2017.26.
  9. K. Bhargavan, V. Cheval, and Ch. A. Wood. A symbolic analysis of privacy for TLS 1.3 with encrypted client hello. In Heng Yin, Angelos Stavrou, Cas Cremers, and Elaine Shi, editors, Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022, pages 365-379. ACM, 2022. URL: https://doi.org/10.1145/3548606.3559360.
  10. B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In 14th IEEE Computer Security Foundations Workshop (CSFW-14 2001), 11-13 June 2001, Cape Breton, Nova Scotia, Canada, pages 82-96. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/CSFW.2001.930138.
  11. B. Blanchet. From secrecy to authenticity in security protocols. In Manuel V. Hermenegildo and Germán Puebla, editors, Static Analysis, 9th International Symposium, SAS 2002, Madrid, Spain, September 17-20, 2002, Proceedings, Lecture Notes in Computer Science, pages 342-359. Springer, 2002. URL: https://doi.org/10.1007/3-540-45789-5_25.
  12. B. Blanchet, M. Abadi, and C. Fournet. Automated Verification of Selected Equivalences for Security Protocols. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pages 331-340, Chicago, IL, June 2005. IEEE Computer Society. URL: https://doi.org/10.1109/LICS.2005.8.
  13. B. Blanchet, V. Cheval, and V. Cortier. ProVerif with lemmas, induction, fast subsumption, and much more. In 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022, pages 69-86. IEEE, 2022. URL: https://doi.org/10.1109/SP46214.2022.9833653.
  14. V. Cheval and B. Blanchet. Proving more observational equivalences with proverif. In David A. Basin and John C. Mitchell, editors, Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, Lecture Notes in Computer Science, pages 226-246. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-36830-1_12.
  15. V. Cheval, V. Cortier, and M. Turuani. A little more conversation, a little less action, a lot more satisfaction: Global states in proverif. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 344-358. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/CSF.2018.00032.
  16. V. Cheval, C. Cremers, A. Dax, L. Hirschi, C. Jacomme, and S. Kremer. Hash gone bad: Automated discovery of protocol attacks that exploit hash function weaknesses. In Joseph A. Calandrino and Carmela Troncoso, editors, 32nd USENIX Security Symposium, USENIX Security 2023, Anaheim, CA, USA, August 9-11, 2023, pages 5899-5916. USENIX Association, 2023. URL: https://www.usenix.org/conference/usenixsecurity23/presentation/cheval.
  17. V. Cheval and S. Delaune. Symbolic protocol verification modulo XOR in ProVerif. In Proceedings of the 2026 ACM SIGSAC Conference on Computer and Communications Security, CCS 2026, The Hague, The Netherlands, November 15-19, 2026. ACM, To appear. Google Scholar
  18. V. Cheval, C. Jacomme, S. Kremer, and R. Künnemann. SAPIC+: protocol verifiers of the world, unite! In K. R. B. Butler and K. Thomas, editors, 31st USENIX Security Symposium, USENIX Security 2022, Boston, MA, USA, August 10-12, 2022, pages 3935-3952. USENIX Association, 2022. URL: https://www.usenix.org/conference/usenixsecurity22/presentation/cheval.
  19. V. Cheval and I. Rakotonirina. Indistinguishability beyond diff-equivalence in ProVerif. In 36th IEEE Computer Security Foundations Symposium, CSF 2023, Dubrovnik, Croatia, July 10-14, 2023, pages 184-199. IEEE, 2023. URL: https://doi.org/10.1109/CSF57540.2023.00036.
  20. Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani. Deciding the security of protocols with Diffie-Hellman exponentiation and product in exponents. In Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'03), volume 2914 of LNCS, pages 124-135, Mumbai (India), 2003. Springer-Verlag. URL: https://doi.org/10.1007/978-3-540-24597-1_11.
  21. Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani. An NP decision procedure for protocol insecurity with XOR. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 261-270. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210066.
  22. R. Chrétien, V. Cortier, and S. Delaune. Decidability of trace equivalence for protocols with nonces. In C. Fournet, M. W. Hicks, and L. Viganò, editors, IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July, 2015, pages 170-184. IEEE Computer Society, 2015. URL: https://doi.org/10.1109/CSF.2015.19.
  23. H. Comon-Lundh and S. Delaune. The finite variant property: How to get rid of some algebraic properties. In Jürgen Giesl, editor, Proc. 16th International Conference on Rewriting Techniques and Applications (RTA'05), volume 3467 of LNCS, pages 294-307, Nara, Japan, 2005. Springer. URL: https://doi.org/10.1007/978-3-540-32033-3_22.
  24. H. Comon-Lundh and V. Shmatikov. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, page 271. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210067.
  25. V. Cortier, A. Dallon, and S. Delaune. A small bound on the number of sessions for security protocols. In 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022, pages 33-48. IEEE, 2022. URL: https://doi.org/10.1109/CSF54842.2022.9919670.
  26. V. Cortier, S. Delaune, and P. Lafourcade. A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur., 14(1):1-43, 2006. URL: https://doi.org/10.3233/JCS-2006-14101.
  27. C. Cremers. The Scyther tool: Verification, falsification, and analysis of security protocols. In A. Gupta and S. Malik, editors, Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings, Lecture Notes in Computer Science, pages 414-418. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70545-1_38.
  28. C. Cremers and M. Dehnel-Wild. Component-based formal analysis of 5G-AKA: Channel assumptions and session confusion. In 26th Annual Network and Distributed System Security Symposium, NDSS 2019, San Diego, California, USA, February 24-27, 2019. The Internet Society, 2019. URL: https://www.ndss-symposium.org/ndss-paper/component-based-formal-analysis-of-5g-aka-channel-assumptions-and-session-confusion/.
  29. C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe. A comprehensive symbolic analysis of TLS 1.3. In B. Thuraisingham, D. Evans, T. Malkin, and D. Xu, editors, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017, pages 1773-1788. ACM, 2017. URL: https://doi.org/10.1145/3133956.3134063.
  30. S. Delaune. An undecidability result for AGh. Theoretical Computer Science, 368(1-2):161-167, 2006. URL: https://doi.org/10.1016/j.tcs.2006.08.018.
  31. S. Delaune, P. Lafourcade, D. Lugiez, and R. Treinen. Symbolic protocol analysis in presence of a homomorphism operator and Exclusive Or. In M. Bugliesi, B. Preneel, V. Sassone, and I. Wegener, editors, Automata, Languages and Programming, 33rd International Colloquium, ICALP 2006, Venice, Italy, July 10-14, 2006, Proceedings, Part II, Lecture Notes in Computer Science, pages 132-143. Springer, 2006. URL: https://doi.org/10.1007/11787006_12.
  32. D. Dolev, S. Even, and R. M. Karp. On the security of ping-pong protocols. In Proc. Advances in Cryptology (CRYPTO'82), pages 177-186, Santa Barbara (California, USA), 1982. Google Scholar
  33. D. Dolev and A. Chi-Chih Yao. On the security of public key protocols (extended abstract). In 22nd Annual Symposium on Foundations of Computer Science, Nashville, Tennessee, USA, 28-30 October 1981, pages 350-357. IEEE Computer Society, 1981. URL: https://doi.org/10.1109/SFCS.1981.32.
  34. J. Dreier, L. Hirschi, S. Radomirovic, and R. Sasse. Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018, pages 359-373. IEEE Computer Society, 2018. URL: https://doi.org/10.1109/CSF.2018.00033.
  35. J. Dreier, P. Lafourcade, and D. Mahmoud. Shaken, not stirred - automated discovery of subtle attacks on protocols using mix-nets. In Davide Balzarotti and Wenyuan Xu, editors, 33rd USENIX Security Symposium, USENIX Security 2024, Philadelphia, PA, USA, August 14-16, 2024. USENIX Association, 2024. URL: https://www.usenix.org/conference/usenixsecurity24/presentation/dreier.
  36. N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. Workshop on Formal Methods and Security Protocols (FMSP'99) - FLOC Workshop, Trento (Italy), 1999. Google Scholar
  37. S. B. Fröschle. Leakiness is decidable for well-founded protocols. In R. Focardi and A. C. Myers, editors, Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, Lecture Notes in Computer Science, pages 176-195. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46666-7_10.
  38. Tamarin GitHub. Bug in built-in XOR (issue 770). https://github.com/tamarin-prover/tamarin-prover/issues/770, 2025.
  39. É. Klein. Formal Verification in Practice: Real-World Case Study and Enhanced Support for AC Operators in Tamarin. PhD thesis, University of Lorraine, Nancy, France, 2025. Google Scholar
  40. N. Kobeissi, K. Bhargavan, and B. Blanchet. Automated verification for secure messaging protocols and their implementations: A symbolic and computational approach. In 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26-28, 2017, pages 435-450. IEEE, 2017. URL: https://doi.org/10.1109/EuroSP.2017.38.
  41. R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. In P. Ning, P. F. Syverson, and S. Jha, editors, Proceedings of the 2008 ACM Conference on Computer and Communications Security, CCS 2008, Alexandria, Virginia, USA, October 27-31, 2008, pages 129-138. ACM, 2008. URL: https://doi.org/10.1145/1455770.1455788.
  42. R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the Horn theory based approach. J. Autom. Reason., 46(3-4):325-352, 2011. URL: https://doi.org/10.1007/S10817-010-9188-8.
  43. S. Meier, B. Schmidt, C. Cremers, and D. A. Basin. The Tamarin prover for the symbolic analysis of security protocols. In N. Sharygina and H. Veith, editors, Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science, pages 696-701. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39799-8_48.
  44. R. Ramanujam and S. P. Suresh. Tagging makes secrecy decidable for unbounded nonces as well. In Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'03), volume 2914 of LNCS, pages 363-374, Mumbai (India), 2003. Springer-Verlag. Google Scholar
  45. M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In Proc. 14th Computer Security Foundations Workshop (CSFW'01), pages 174-190, Cape Breton (Canada), 2001. IEEE Comp. Soc. Press. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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