Keynote Speakers
Title: miTLS: Can cryptography, formal methods, and applied security be friends?
Dr. Markulf Kohlweiss, Researcher, Microsoft Research
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.
Speaker Bio
Dr. Markulf Kohlweiss is a researcher at Microsoft Research Cambridge in the Programming Principles and Tools group. He did his PhD at the COSIC (Computer Security and Industrial Cryptography) group at the K.U. Leuven, and his master thesis at IBM Research Zurich. Dr. Kohlweiss' research focus is on privacy-enhancing cryptography and formal reasoning about cryptographic protocols. More specifically, he examines the interplay of cryptography and real-world security systems through collaborative projects on verifiable computation and SSL/TLS. For the latter work he is a co-recipient of the Levchin Price awarded to the miTLS team.
Keynote Speakers
- Prof. Swarat Chaudhuri, Rice University
- Dr. Markulf Kohlweiss, Researcher, Microsoft Research
- Dr. Rajeev K. Ranjan, Senior Group Director, R&D Formal and Automated verification, Cadence
- Prof. Andreas Veneris, University of Toronto