ProVerif is a software tool for
automated reasoning
In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer prog ...
about the security properties found in
cryptographic protocol
A security protocol (cryptographic protocol or encryption protocol) is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol descr ...
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 is the property of two or more underlying entities being indistinguishable on the basis of their observable implications. Thus, for example, two scientific theories are observationally equivalent if all of their empiricall ...
. 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 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
In computing, Internet Key Exchange (IKE, sometimes IKEv1 or IKEv2, depending on version) is the protocol used to set up a security association (SA) in the IPsec protocol suite. IKE builds upon the Oakley protocol and ISAKMP.The Internet Key Exch ...
(IKE) as the key exchange protocol in
IPsec
In computing, Internet Protocol Security (IPsec) is a secure network protocol suite that authenticates and encrypts packets of data to provide secure encrypted communication between two computers over an Internet Protocol network. It is used in ...
, 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 (TLS) is a cryptographic protocol designed to provide communications security over a computer network. The protocol is widely used in applications such as email, instant messaging, and voice over IP, but its use in securi ...
(TLS) protocol has been studied in this manner.
* Chen & Ryan have evaluated authentication protocols found in the
Trusted Platform Module
Trusted Platform Module (TPM, also known as ISO/IEC 11889) is an international standard for a secure cryptoprocessor, a dedicated microcontroller designed to secure hardware through integrated cryptographic keys. The term can also refer to a ...
(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 (also known as e-voting) is voting that uses electronic means to either aid or take care of casting and counting ballots.
Depending on the particular implementation, e-voting may use standalone ''electronic voting machines'' ( ...
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 (DAA) is a cryptographic primitive which enables remote authentication of a trusted computer whilst preserving privacy of the platform's user. The protocol has been adopted by the Trusted Computing Group (TCG) in the l ...
(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.
* Google verified its transport layer protocol
ALTS.
*Sardar et al.
verified the remote attestation protocols in
Intel SGX Intel Software Guard Extensions (SGX) is a set of security-related instruction codes that are built into some Intel central processing units (CPUs). They allow user-level and operating system code to define protected private regions of memory, cal ...
.
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.
References
External links
* {{Official website, http://prosecco.gforge.inria.fr/personal/bblanche/proverif/
Cryptographic software
Free software