(... to be written)

Sources

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.

Literature

• [ProVerif] ProVerif: Cryptographic protocol verifier in the formal model
• [BSCS18] Bruno Blanchet, Ben Smyth, Vincent Cheval, Marc Sylvestre: ProVerif 2.00, Automatic Cyptographic Protocol Verifier, User Manual and Tutorial, May 16, 2018.
• [FStar] F*: A Higher-Order Effectful Language Designed for Program Verification
• [OCaml] The OCaml System
• [DY83] Danny Dolev, Andrew C. Yao: On the Security of Public Key Protocols. In: IEEE Transactions on Information Theory, Vol. IT-29, No. 2, March 1983. (full pdf)
• [B09] Bruno Blanchet: Using Horn Clauses for Analyzing Security Protocols. In: Véronique Cortier and Steve Kremer, editors, Formal Models and Techniques for Analyzing Security Protocols, volume 5 of Cryptology and Information Security Series, pages 86-111. IOS Press, March 2011. (full pdf)
• [B10] Bruno Blanchet: The automatic security protocol verifier ProVerif. June 2010. (slides pdf)
• [B16] Bruno Blanchet: Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. In: Foundations and Trends in Privacy and Security, Volume 1 Issue 1-2, 31 10 2016, pages 1-135 (paywalled version, full pdf)
• [ABF18] Martín Abadi, Bruno Blanchet, Cédric Fournet: The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication. In: Journal of the ACM, Volume 65 Issue 1, January 2018, Article No. 1. (acm.org pdf available, older pdf at arxiv.org)
• [BBK17] Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi: Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In: 2017 IEEE Symposium on Security and Privacy. (full pdf)
• [RefTLS] Symbolic Verification with ProVerif. Project Website.