Skip to Main content Skip to Navigation
New interface
Conference papers

ProVerif with Lemmas, Induction, Fast Subsumption, and Much More

Bruno Blanchet 1 Vincent Cheval 2, 1 Véronique Cortier 2 
2 PESTO - Proof techniques for security protocols
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents a major overhaul of one the most widely used symbolic security protocol verifiers, ProVerif. We provide two main contributions. First, we extend ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we rework and optimize many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption,. . .), resulting in impressive speed-ups on large examples.
Document type :
Conference papers
Complete list of metadata
Contributor : Véronique Cortier Connect in order to contact the contributor
Submitted on : Thursday, October 7, 2021 - 9:22:24 AM
Last modification on : Wednesday, June 8, 2022 - 12:50:05 PM
Long-term archiving on: : Saturday, January 8, 2022 - 6:06:56 PM



  • HAL Id : hal-03366962, version 1



Bruno Blanchet, Vincent Cheval, Véronique Cortier. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. S&P 2022 - 43rd IEEE Symposium on Security and Privacy, May 2022, San Francisco, United States. ⟨hal-03366962⟩



Record views


Files downloads