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

Authors: Stéphanie Delaune

Open access: https://doi.org/10.4230/LIPIcs.LICS.2026.2

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.

BibTeX

  @InProceedings{Delaune-FormalVerificationo,
    author = 	 {Stéphanie Delaune},
    title = 	 {Formal Verification of Security Protocols: 25 Years of ProVerif},
    booktitle =  {Proceedings of the Forty-First Annual Symposium on Logic in Computer Science (LICS 2026)},
    year =	 {2026},
    month =	 {July}, 
    pages =      {2:1--2:9},
    location =   {Lisbon, Portugal}, 
    note =       {Invited Talk},
    publisher =	 {Schloss Dagstuhl -- Leibniz-Zentrum für Informatik},
    doi =        {10.4230/LIPIcs.LICS.2026.2}
  }