ACE Seminar: Triple Handshake: Can cryptography, formal methods, and applied security be friends?

Speaker: Dr Markulf Kohlweiss

Date/Time: 12-Mar-2015, 16:00 UTC

Venue: MPEB 1.03



TLS was designed as a transparent channel abstraction to allow developers with no cryptographic expertise to protect their application against attackers that may control some clients, some servers, and may have the capability to tamper with network connections. However, the security guarantees of TLS fall short of those of a secure channel, leading to a variety of attacks. The Triple Handshake attack exploits combinations of RSA and Diffie-Hellman key exchange, session resumption, and renegotiation to bypass many recent countermeasures.

At the same time we study the provable security of TLS, as it is implemented and deployed. To capture the details of the standard and its main extensions, we rely on miTLS, a verified reference implementation of the protocol. miTLS inter-operates with mainstream browsers and servers for many protocol versions, configurations, and ciphersuites; and it provides application-level, provable security for some.

This leads to the strange case of how something provable secure can be insecure. In this talk I will play Dr Jekyll and Mr Hyde by playing off our CRYPTO proof and our S&P attack against each other.


I am a researcher at Microsoft Research, Cambridge, in the Programming Principles and Tools group and a member of the Constructive Security subgroup. I did my PhD at COSIC (Computer Security and Industrial Cryptography) group at the Department of Electrical Engineering ESAT of the K.U.Leuven on Privacy Enhancing Cryptography. I am currently working on verifiable computation, zero-knowledge proofs and malleability, and formal verification of cryptographic protocols.

Add to Calendar

This page was last modified on 27 Mar 2014.