(... to be written)


This crypto bite is based almost entirely on ProVerif's User Manual[BSCS18], on Bruno Blanchet's papers and presentations/slides, and on Karthik's talk (see below).

The theoretical background of ProVerif[ProVerif] and the underlying pi calculus are explained in [B16, ABF18]. ProVerif is based on the F* language[FStar], which itself is an extension to OCaml[OCaml]. Like all provers in the symbolic model, ProVerif is also based on the Dolev-Yao model[DY83].

ProVerif has been used to verify TLS 1.3 Standard Canditates in the symbolic model[BBK17, RefTLS].

Karthikeyan Bhargavan gave an introduction to ProVerif in his talk "Automated Symbolic Protocol Verification" (slides) at the 8th BIU Winter School on Cryptography, Secure Key Exchange, February 11-15 2018 (all videos):

The talk on ProVerif resumes in the followup session "Mechanized Computational Protocol Proofs" up to 21:53 (after that, it's about CryptoVerif):

The context of Karthik's talk was Secure Key Exchange, though ProVerif has of course been used to verify more protocols than merely key exchange protocols.