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-)