LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Automated Computational Verification for Cryptographic Protocol Implementations

 Eugen Zalinescu
Tuesday, April 28 2009 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Eugen Zalinescu (Microsoft Research-INRIA)

We automatically verify implementations of cryptographic protocols programmed in ML. We develop a prototype compiler from a subset of ML to CryptoVerif, Blanchet's prover for computational cryptography. Thus, we obtain a first tool chain that yields security guarantees for computational models tightly related to executable code. We show the soundness of the underlying translation for authentication and secrecy. To this end, we equip ML programs with a probabilistic semantics, and relate it to the probabilistic polynomial-time semantics of CryptoVerif. We also review experimental (symbolic and computational) results recently obtained for a reference implementation of the TLS protocol.

(This is joint work with Karthik Bhargavan, Ricardo Corin, and Cédric Fournet.)

About LSV