Section: Software

ProVerif

Participant : Bruno Blanchet.

ProVerif (http://www.proverif.ens.fr/ ) is an automatic security protocol verifier, in the formal model (so called Dolev–Yao model). In this model, cryptographic primitives are considered as black boxes. This protocol verifier is based on an abstract representation of the protocol by Horn clauses. Its main features are:

• It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signatures), hash functions, and Diffie–Hellman key agreements, specified both as rewrite rules or as equations.

• It can handle an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space. This result has been obtained thanks to some well-chosen approximations. This means the verifier can give false attacks, but if it claims that the protocol satisfies some property, then the property is actually satisfied. ProVerif also provides attack reconstruction: when it cannot prove a property, it tries to reconstruct an attack, that is, an execution trace of the protocol that falsifies the desired property.

The ProVerif verifier can prove the following properties:

• secrecy (the adversary cannot obtain the secret);

• authentication and more generally correspondence properties, of the form “if an event has been executed, then other events have been executed as well”;

• strong secrecy (the adversary does not see the difference when the value of the secret changes);

• equivalences between processes that differ only by terms;

ProVerif has been used by researchers for studying various kinds of protocols, including electronic voting protocols, certified email protocols, and zero-knowledge protocols. It has been used as a back-end for the tool TulaFale implemented at Microsoft Research Cambridge, which verifies web services protocols. It has also been used as a back-end for verifying implementations of protocols in F# (a dialect of ML included in .NET), by Microsoft Research Cambridge and the joint INRIA-Microsoft research center.

ProVerif is freely available on the web, at http://www.proverif.ens.fr/ , under the GPL license.