ProVerif is a software tool for automated reasoning

Automated reasoning

Automated reasoning is an area of computer science dedicated to understand different aspects of reasoning. The study in automated reasoning helps produce software which allows computers to reason completely, or nearly completely, automatically...

 about the security properties found in cryptographic protocol

Cryptographic protocol

A security protocol is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods.A protocol describes how the algorithms should be used...

s. The tool has been developed by Bruno Blanchet.

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

Observational equivalence

In econometrics, two parameter values are considered observationally equivalent if they both result in the same probability distribution of observable data...

. These reasoning capabilities are particular 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 used correspondence assertions to verify the certified email protocol.
• Abadi, Blanchet & Fournet analyse the Just Fast Keying protocol, which was one of the candidates to replace Internet Key Exchange
  Internet key exchange
  Internet Key Exchange is the protocol used to set up a security association in the IPsec protocol suite. IKE builds upon the Oakley protocol and ISAKMP...
  
   (IKE) as the key exchange protocol in IPsec
  IPsec
  Internet Protocol Security is a protocol suite for securing Internet Protocol communications by authenticating and encrypting each IP packet of a communication session...
  
  , by combining manual proofs with ProVerif proofs of correspondence and equivalence.
• Blanchet & Chaudhuri studied the integrity of the Plutus file system on untrusted storage, using correspondence assertions, resulting in the discovery, and subsequent fixing, of weaknesses in the initial system.
• Bhargavan et al. use ProVerif to analyse cryptographic protocol implementations written in the F Sharp (programming language); in particular the Transport Layer Security
  Transport Layer Security
  Transport Layer Security and its predecessor, Secure Sockets Layer , are cryptographic protocols that provide communication security over the Internet...
  
   (TLS) protocol has been studied in this manner.
• Chen & Ryan have evaluated authentication protocols found in the Trusted Platform Module
  Trusted Platform Module
  In computing, Trusted Platform Module is both the name of a published specification detailing a secure cryptoprocessor that can store cryptographic keys that protect information, as well as the general name of implementations of that specification, often called the "TPM chip" or "TPM Security...
  
   (TPM), a widely deployed hardware chip, and discovered vulnerabilities.
• Delaune, Kremer & Ryan and Backes, Hritcu & Maffei formalise and analyse privacy properties for electronic voting
  Electronic voting
  Electronic voting is a term encompassing several different types of voting, embracing both electronic means of casting a vote and electronic means of counting votes....
  
   using observational equivalence.
• Delaune, Ryan & Smyth and Backes, Maffei & Unruh analyse the anonymity properties of the trusted computing scheme Direct Anonymous Attestation
  Direct anonymous attestation
  The Direct Anonymous Attestation is a cryptographic protocol which enables the remote authentication of a trusted platform whilst preserving the user's privacy...
  
   (DAA) using observational equivalence.
• Kusters & Truderung examine protocols with Diffie-Hellman exponentiation and XOR.
• Smyth, Ryan, Kremer & Kourjieh formalise and analyse verifiability properties for electronic voting using reachability.

Further examples can be found online: http://www.proverif.ens.fr/proverif-users.html.

Alternatives

Alternative analysis tools include: AVISPA (for reachability and correspondence assertions), KISS (for static equivalence), YAPA (for static equivalence). CryptoVerif

CryptoVerif

CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet. Contrary to ProVerif by the same creator that uses a symbolic abstraction, it is sound in the computational model.It can prove...

 for verification of security agains polynomial time adversaries in the computational model.