BlanchetEtAlSP22

Bruno Blanchet Back to publications

Bruno Blanchet, Vincent Cheval, and Véronique Cortier. ProVerif with lemmas, induction, fast subsumption, and much more. In IEEE Symposium on Security and Privacy (S&P'22), pages 205-222, San Francisco, CA, May 2022. IEEE Computer Society.

Get the paper

.pdf, 423 Kb

Links

Long version and benchmarks

Official version

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{BlanchetEtAlSP22,
  AUTHOR = {Blanchet, Bruno and Cheval, Vincent and Cortier, V{\'e}ronique},
  TITLE = {{P}ro{V}erif with lemmas, induction, fast subsumption, and much more},
  BOOKTITLE = {IEEE Symposium on Security and Privacy (S\&P'22)},
  YEAR = 2022,
  PAGES = {205--222},
  MONTH = MAY,
  ADDRESS = {San Francisco, CA},
  PUBLISHER = {IEEE Computer Society}
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)