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.
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
(This is joint work with Karthik Bhargavan, Ricardo Corin, and Cédric Fournet.)