Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Automated Computational Verification for Cryptographic Protocol Implementations

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Eugen Zalinescu
Date
Le mardi 28 avril 2009 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
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.)


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents