CryptoForma and BCS-FACS joint event, 15 January 2014

CryptoForma comes to the BCS headquarters, during the afternoon an open workshop, in the evening a talk in the regular BCS-FACS evening seminar series for a wider formal methods audience by Cédric Fournet.

14:00 Afternoon programme

18:00 Verified Reference Implementation of TLS (BCS-FACS, January 2014)

Speaker: Dr. Cédric Fournet (Microsoft Research Cambridge & MSR-INRIA Research Centre)

TLS (Transport Layer Security) is the most widely deployed protocol for securing communications, e.g. used in HTTPS secure web connections. Yet, after two decades of attacks, patches, and extensions, its practical security remains controversial. In my presentation, I will
(1) illustrate why TLS is so difficult to get right, using recent attacks against the protocol, its underlying cryptography, and its typical usage in web applications; and
(2) present our research of TLS security, centred on a new verified reference implementation of the Internet standard coded in F#. Our codebase interoperates with mainstream browsers and servers, with reasonable performance. At the same time, our code is carefully structured to enable its modular, automated verification, from its main API down to cryptographic assumptions on e.g. AES and RSA.
This is joint work at the MSR INRIA research centre, with Karthik Bhargavan, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, and Santiago Zanella.
See (running our own TLS server) for papers, attacks, code, and details.

BCS London Offices, First Floor
The Davidson Building
5 Southampton Street London WC2E 7HA

Refreshments will be served from 5.15pm.

The seminar comes at the end of a regular meeting of the EPSRC CryptoForma network ( on Formal Methods and Cryptography. Both this meeting and the seminar are free of charge and open to everyone.
If you would like to attend the seminar, please register as soon as possible at Pre-registration is required, as security at the BCS Offices is tight.
(If you would also like to attend the rest of the day, please also inform the CryptoForma coordinator, Eerke Boiten

BCS-FACS Website:
Location of venue:


Stay updated

Stay involved in our discussions on various social networks.

Comments are closed.