ICSA Colloquium Talk - 23/03/2023

Speaker: Dr. Abhishek Bichhawat

Talk Title: Are you messaging securely?

Abstract: While many messaging apps claim end-to-end security of the exchanged messages, there are no formal guarantees offered by the applications regarding the same. To this end, we have built DY* (https://reprosec.org/dystar/), which is a formal verification framework for the symbolic security analysis of cryptographic protocol code written in the F* programming language. Unlike existing automated symbolic provers, our framework accounts for advanced protocol features like unbounded loops and mutable recursive data structures, as well as low-level implementation details like protocol state machines and message formats, which are often at the root of real-world attacks. We have demonstrated the effectiveness of our framework through several in-depth symbolic security analyses of protocols like Signal, ISO-DH, ACME and Noise. In this talk, I will discuss the DY* framework, and a couple of protocols that we have verified in the framework.

Bio: Abhishek Bichhawat is an Assistant Professor in the Discipline of Computer Science and Engineering at IIT Gandhinagar, India. His research is primarily focused on building secure systems by design while providing formal security guarantees about real systems, with an emphasis on creating solid foundations for practical solutions.