@inproceedings{CKR-sp18,
  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.},
  author =	 {Blanchet, Bruno and Cheval, Vincent and Cortier V{\'e}ronique},
  booktitle =	 {{P}roceedings of the 43th IEEE Symposium on Security
                  and Privacy (S\&P'22)},
  month =	 may,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {ProVerif with Lemmas, Induction, Fast Subsumption, and Much More},
  year =	 2022,
  acronym =	 {{S\&P}'22},
}