ProVerif: Cryptographic protocol verifier in the symbolic model

ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a 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 that the verifier can give false attacks, but if it claims that the protocol satisfies some property, then the property is actually satisfied.

This verifier can prove the following properties:

• secrecy (the adversary cannot obtain the secret, CSFW'01)
• authentication and more generally correspondence properties (Journal of Computer Security, 17(4):363-434, 2009)
• strong secrecy (the adversary does not see the difference when the value of the secret changes, IEEE S&P'04)
• equivalences between processes that differ only by terms (Journal of Logic and Algebraic Programming, 75(1):3-51, 2008 with Martín Abadi and Cédric Fournet)