Chennai Mathematical Institute


Lecture Announcement
Date: Tuesday, May 10, 2022
Time: 1400 -- 1500
Venue: Lecture Hall 5, CMI (hybrid mode)
Verified Implementations for Real-World Cryptographic Protocols

Karthikeyan Bhargavan


The security of the Web relies on cryptographic protocols, i.e. distributed programs that use cryptography to protect sensitive data against subtle attacks from powerful adversaries that fully control the network. However, despite decades of careful study, theoretical and practical attacks continue to be found in real-world cryptographic protocols like Transport Layer Security (TLS). In this seminar, we will look at what goes wrong in these protocols, and we will discuss how formal verification can be used to eliminate certain classes of attacks against implementations of modern protocols like TLS 1.3 and Signal.

About the Speaker:

Karthikeyan Bhargavan is a researcher at INRIA, where he leads a group called Prosecco (Programming Securely with Cryptography). He received his B.Tech from IIT Delhi in 1997, his PhD from the University of Pennsylvania in 2003, and worked as a researcher in Microsoft Research Cambridge before joining INRIA in 2009. Bhargavan is interested in the design and implementation of program verification techniques that enable robust implementations and formal analyses of real-world security applications. His recent work focuses on using dependent type systems, such as F*. to investigate the (in)security of cryptographic protocols, such as Transport Layer Security (TLS), and to build verified cryptographic libraries, such as HACL*. For more details on the Prosecco research group and it publications, see