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
- Date
- Tuesday, April 28 2009 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.)