ProVerif

ProVerif is a software tool for automated reasoning about the security properties of cryptographic protocols. The tool has been developed by Bruno Blanchet and others.

ProVerif

Developer(s)	Bruno Blanchet
Initial release	June 1, 2002 (2002-06-01)
Stable release	2.04 / December 1, 2021 (2021-12-01)[1]
Written in	OCaml
Available in	English
License	Mainly, GNU GPL; Windows binaries, BSD licenses
Website	prosecco.gforge.inria.fr/personal/bblanche/proverif/

Support is provided for cryptographic primitives including: symmetric & asymmetric cryptography; digital signatures; hash functions; bit-commitment; and signature proofs of knowledge. The tool is capable of evaluating reachability properties, correspondence assertions and observational equivalence. These reasoning capabilities are particularly useful to the computer security domain since they permit the analysis of secrecy and authentication properties. Emerging properties such as privacy, traceability and verifiability can also be considered. Protocol analysis is considered with respect to an unbounded number of sessions and an unbounded message space. The tool is capable of attack reconstruction: when a property cannot be proved, an execution trace which falsifies the desired property is constructed.

Applicability of ProVerif

ProVerif has been used in the following case studies, which include the security analysis of actual network protocols:

• Abadi & Blanchet^[2] used correspondence assertions to verify the certified email protocol.^[3]
• Abadi, Blanchet & Fournet^[4] analyse the Just Fast Keying^[5] protocol, which was one of the candidates to replace Internet Key Exchange (IKE) as the key exchange protocol in IPsec, by combining manual proofs with ProVerif proofs of correspondence and equivalence.
• Blanchet & Chaudhuri^[6] studied the integrity of the Plutus file system^[7] on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
• Bhargavan et al.^[8][9][10] use ProVerif to analyse cryptographic protocol implementations written in F#; in particular the Transport Layer Security (TLS) protocol has been studied in this manner.
• Chen & Ryan^[11] have evaluated authentication protocols found in the Trusted Platform Module (TPM), a widely deployed hardware chip, and discovered vulnerabilities.
• Delaune, Kremer & Ryan^[12][13] and Backes, Hritcu & Maffei^[14] formalise and analyse privacy properties for electronic voting using observational equivalence.
• Delaune, Ryan & Smyth^[15] and Backes, Maffei & Unruh^[16] analyse the anonymity properties of the trusted computing scheme Direct Anonymous Attestation (DAA) using observational equivalence.
• Kusters & Truderung^[17][18] examine protocols with Diffie-Hellman exponentiation and XOR.
• Smyth, Ryan, Kremer & Kourjieh^[19] formalise and analyse verifiability properties for electronic voting using reachability.
• Google^[20] verified its transport layer protocol ALTS.
• Sardar et al.^[21][22] verified the remote attestation protocols in Intel SGX.

Further examples can be found online: .

Alternatives

Alternative analysis tools include: AVISPA (for reachability and correspondence assertions), KISS (for static equivalence), YAPA (for static equivalence). CryptoVerif for verification of security against polynomial time adversaries in the computational model. The Tamarin Prover is a modern alternative to ProVerif, with excellent support for Diffie-Hellman equational reasoning, and verification of observational equivalence properties.