BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:From crypto verif specifications to computationally secure impleme
 ntations of protocols - Blanchet\, B (ENS)
DTSTART:20120411T123000Z
DTEND:20120411T133000Z
UID:TALK37409@talks.cam.ac.uk
CONTACT:Mustapha Amrani
DESCRIPTION:CryptoVerif is a protocol verifier in the computational model\
 , which generates proofs by sequences of games\, like those written manual
 ly by cryptographers.  We have implemented a compiler that automatically t
 ranslates CryptoVerif specifications into implementations of protocols\, i
 n the OCaml language. The goal of this compiler is to generate implementat
 ions of security protocols proved secure in the computational model: from 
 the same specification\, we can prove it using CryptoVerif and generate th
 e implementation using our compiler.  We are currently using this framewor
 k in order to generate an implementation of SSH.\n
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR