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

Bruno Blanchet, Vincent Cheval, and Véronique Cortier. ProVerif with Lemmas, Induction, Fast Subsumption, and Much More. In Proceedings of the 42nd IEEE Symposium on Security and Privacy (S&P'22), IEEE Computer Society Press, 2022.
doi:10.1109/SP.2017.28

Download

[PDF] [PDF (long version)] [HTML] 

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.

BibTeX

@InProceedings{proverif-SP22,
  author =	 {Bruno Blanchet and Vincent Cheval and V\'eronique
                  Cortier},
  title =	 {ProVerif with Lemmas, Induction, Fast Subsumption,
                  and Much More},
  booktitle =	 {{P}roceedings of the 42nd IEEE Symposium on Security
                  and Privacy (S\&P'22)},
  year =	 2022,
  publisher =	 {{IEEE} Computer Society Press},
  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.  },
  doi =		 {10.1109/SP.2017.28},
                  ={https://members.loria.fr/VCortier/files/Papers/SP22.pdf},
                  ={https://bblanche.gitlabpages.inria.fr/proverif/snp22/},
}