Automatic Verification of Security Protocols

Go Back to Talks and Events

Talk by Dr. Bruno Blanchet ,CNRS, Ecole Normale Supperieure.
Time: July 10, 2pm Place: Rm.2311 (CS Wireless Seminar Room), Computer Science Building

CryptoVerif: A Computationally Sound Mechanized Prover for Security Protocols

We will present the prover CryptoVerif and briefly compare with other protocol provers, in particular our other prover ProVerif.

CryptoVerif is the first mechanized prover for security protocols sound in the computational model. It produces proofs presented as sequences of games, like the manual proofs of cryptographers; these games are formalized in a probabilistic polynomial-time process calculus. CryptoVerif provides a generic method for specifying security assumptions on cryptographic primitives, which can handle shared-key and public-key encryption, signatures, message authentication codes, and hash functions. It can prove secrecy and correspondence properties (including authentication). It produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary.

Bio: Bruno Blanchet received his BSc and MSc degrees in computer science from Ecole Normale Superieure, Paris, France in 1995 and 1996, respectively. He did his PhD at INRIA Rocquencourt under the supervision of Patrick Cousot and Alain Deutsch and received his PhD degree from Ecole Polytechnique in 2000. He was an independent research group leader at the Max-Planck-Institut for Computer Science, Saarbrucken, Germany from 2001 to 2004. Since 2001, he has been researcher at CNRS, Ecole Normale Supperieure. His main research interest is automatic program analysis for verification, in particular the formal verification of security protocols.