BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cryptographically verified implementation of TLS 1.2 - Fournet\, C
  (Microsoft Research)
DTSTART:20120413T123000Z
DTEND:20120413T133000Z
UID:TALK37466@talks.cam.ac.uk
CONTACT:Mustapha Amrani
DESCRIPTION:Joint work with Karthik Bhargavan\, Markulf Kohlweiss\, Alfred
 o Pironti\, and Pierre-Yves Strub\n\nWe develop a reference implementation
  of the TLS 1.2 Internet Standard. \nOur code fully supports binary wire f
 ormats\, multiple ciphersuites\, sessions and connections with re-handshak
 es and resumptions\, alerts\, message fragmentation\, ... as prescribed by
  the standard\; it interoperates with other implementations\, notably exis
 ting web browsers and servers. At the same time\, our code is carefully st
 ructured to enable its automated\, modular verification\, from its main AP
 I down to computational security assumptions on its underlying cryptograph
 ic algorithms.\n\nIn the talk\, I will review our modular cryptographic ve
 rification method\, which is based on F7\, a refinement type checker coupl
 ed with an SMT-solver\, with a theory formalized in Coq. Using F7\, we ver
 ify constructions and protocols coded in F# by typing them against new cry
 ptographic interfaces that capture their authenticity and secrecy properti
 es. We relate their ideal functionalities and concrete implementations\, u
 sing game-based program transformations behind typed interfaces\, so that 
 we can easily compose them.\n\nI will also outline our TLS implementations
 \, coded in F# and specified in F7. I will present its main typed interfac
 es\, which can be read as specifications of "giant" ideal functionalities 
 for its main components\, such as authenticated encryption for the record 
 layer and key establishment for the handshake. I will finally describe our
  main security results\, as well as some new attacks we found in the proce
 ss.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR