@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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},
  OPTpages = 	 {},
  OPTmonth = 	 {},
  OPTaddress = 	 {},
  OPTorganization = {},
  publisher = {{IEEE} Computer Society Press},
  OPTannote = 	 {},
  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.
},
OPTdoi = {10.1109/SP.2017.28},
}