The verifier ProVerif is based on the formal model of cryptography. Dolev-Yao model). In this model, cryptographic primitives are considered as black boxes. ProVerif is based on an abstract representation of the protocol by Horn clauses. It can handle many different cryptographic primitives, specified both as rewrite rules or as equations. It can handle an unbounded number of sessions of the protocol and an unbounded message space. It can prove secrecy properties, correspondences (authentication) and some process equivalences.
The verifier CryptoVerif is based on the computational model of cryptography. In this model, messages are bitstrings and cryptographic primitives are functions on bitstrings. CryptoVerif generates proofs by sequences of games, as used by cryptographers. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. CryptoVerif provides a generic mechanism for specifying the security assumptions on cryptographic primitives. It can also evaluate the probability of breaking the protocol as a function of the probability of breaking each cryptographic primitive and of the number of sessions.
@PHDTHESIS{BlanchetHDR,
AUTHOR = {Bruno Blanchet},
TITLE = {Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. Automatic verification of security protocols: formal model and computational model},
SCHOOL = {Université Paris-Dauphine},
YEAR = 2008,
TYPE = {Mémoire d'habilitation à diriger des recherches},
MONTH = NOV,
NOTE = {En français avec publications en anglais en annexe. In French with publications in English in appendix.}
}