ProVerif: Automated Protocol Verification

ProVerif (Bruno Blanchet, 2001) is an automated cryptographic protocol verifier. It takes a protocol described in applied pi calculus and automatically decides secrecy and authentication properties.

ProVerif translates the protocol into Horn clauses and applies a resolution-based algorithm to derive what the attacker can learn. If a secrecy fact is derivable, the protocol is broken; otherwise, it is proved secure.