(... to be written)
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].
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 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.
- [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.