ProVerif is a software tool for automated reasoning about the security properties of cryptographic protocols. It has been developed by Bruno Blanchet and others, with its initial release on June 1, 2002. The tool is written in OCaml and is available under the GNU GPL license (with BSD licensing for Windows binaries).
Overview
ProVerif operates within the formal Dolev-Yao model (symbolic model) of security. It uses an abstract representation of protocols via Horn clauses and applies a resolution algorithm on these clauses to prove security properties or find attacks. The tool supports analysis with respect to an unbounded number of sessions and an unbounded message space.
Supported Cryptographic Primitives
ProVerif provides support for a wide range of cryptographic primitives, including:
- Symmetric and asymmetric encryption
- Digital signatures
- Hash functions
- Bit-commitment
- Non-interactive zero-knowledge proofs
Security Properties
The tool can evaluate three main types of security properties:
- Reachability properties – determining whether certain states or actions are reachable
- Correspondence assertions – used to analyze authentication properties
- Observational equivalence – used to analyze privacy, anonymity, and secrecy properties
When a property cannot be proved, ProVerif can reconstruct an execution trace that falsifies the desired property, helping identify potential attacks.
Notable Applications
ProVerif has been applied to numerous real-world security analyses, including:
- Analysis of the Transport Layer Security (TLS) protocol
- Verification of Google's Application Layer Transport Security (ALTS)
- Analysis of the Just Fast Keying protocol (a candidate to replace IKE in IPsec)
- Verification of remote attestation protocols in Intel SGX
- Analysis of authentication protocols in the Trusted Platform Module (TPM), where vulnerabilities were discovered
- Formal analysis of electronic voting protocols for privacy and verifiability
- Verification of the certified email protocol
- Analysis of the Direct Anonymous Attestation (DAA) scheme for anonymity
Alternatives
Other tools for cryptographic protocol verification include AVISPA (for reachability and correspondence assertions), CryptoVerif (for verification in the computational model against polynomial-time adversaries), and the Tamarin Prover (a modern alternative with support for Diffie-Hellman equational reasoning and observational equivalence).
