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 progr ...

about the security properties of

cryptographic protocol A cryptographic protocol is an abstract or concrete Communications protocol, protocol that performs a information security, security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol desc ...

s. The tool has been developed by Bruno Blanchet and others. Support is provided for

cryptographic primitive Cryptographic primitives are well-established, low-level cryptography, cryptographic algorithms that are frequently used to build cryptographic protocols for computer security systems. These routines include, but are not limited to, one-way hash fun ...

s including:

symmetric Symmetry () in everyday life refers to a sense of harmonious and beautiful proportion and balance. In mathematics, the term has a more precise definition and is usually used to refer to an object that is invariant under some transformations ...

& 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 empirica ...

. These reasoning capabilities are particularly useful to the

computer security Computer security (also cybersecurity, digital security, or information technology (IT) security) is a subdiscipline within the field of information security. It consists of the protection of computer software, systems and computer network, n ...

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, versioned as IKEv1 and IKEv2) 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 Exchange (IKE), RFC 2 ...

(IKE) as the key exchange protocol in IPsec, 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 F#; in particular the

Transport Layer Security Transport Layer Security (TLS) is a cryptographic protocol designed to provide communications security over a computer network, such as the Internet. The protocol is widely used in applications such as email, instant messaging, and voice over ...

(TLS) protocol has been studied in this manner. * Chen & Ryan have evaluated authentication protocols found in the

Trusted Platform Module A Trusted Platform Module (TPM) is a secure cryptoprocessor that implements the ISO/IEC 11889 standard. Common uses are verifying that the boot process starts from a trusted combination of hardware and software and storing disk encryption keys. ...

(TPM), a widely deployed hardware chip, and discovered

vulnerabilities Vulnerability refers to "the quality or state of being exposed to the possibility of being attacked or harmed, either physically or emotionally." The understanding of social and environmental vulnerability, as a methodological approach, involves ...

. * Delaune, Kremer & Ryan and Backes, Hritcu & Maffei formalise and analyse privacy properties for

electronic voting Electronic voting is voting that uses electronic means to either aid or handle casting and counting ballots including voting time. Depending on the particular implementation, e-voting may use standalone '' electronic voting machines'' (also ...

using observational equivalence. * Delaune, Ryan & Smyth and Backes, Maffei & Unruh analyse the

anonymity Anonymity describes situations where the acting person's identity is unknown. Anonymity may be created unintentionally through the loss of identifying information due to the passage of time or a destructive event, or intentionally if a person cho ...

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 ...

(DAA) using observational equivalence. * Kusters & Truderung examine protocols with Diffie-Hellman exponentiation and

XOR Exclusive or, exclusive disjunction, exclusive alternation, logical non-equivalence, or logical inequality is a logical operator whose negation is the logical biconditional. With two inputs, XOR is true if and only if the inputs differ (one ...

. * Smyth, Ryan, Kremer & Kourjieh formalise and analyse verifiability properties for electronic voting using reachability. *

Google Google LLC (, ) is an American multinational corporation and technology company focusing on online advertising, search engine technology, cloud computing, computer software, quantum computing, e-commerce, consumer electronics, and artificial ...

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 instruction codes implementing trusted execution environment that are built into some Intel central processing units (CPUs). They allow user-level and operating system code to define protected priv ...

. 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 In theoretical computer science, the time complexity is the computational complexity that describes the amount of computer time it takes to run an algorithm. Time complexity is commonly estimated by counting the number of elementary operations p ...

adversaries in the computational model. The

Tamarin Prover Tamarin Prover is a computer software program for formal verification of cryptographic protocols. It has been used to verify Transport Layer Security 1.3, ISO/IEC 9798, DNP3 Secure Authentication v5, WireGuard,; and the PQ3 Messaging Protocol ...

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 programmed in OCaml Automated reasoning Software using the GNU General Public License Software using the BSD license