Logics play a large role in the formal study and analysis of systems, especially for formal verification. The exact shape of the syntax and inference rules involved depend heavily on the systems being modelled and verified. In this talk, we will introduce a logical syntax for communicated messages and an associated proof system originally used in the verification of cryptographic protocols, dating back to a very robust model from 1983, which captures even the operational aspects of today’s internet. We will show how to extend this system to be able to better handle protocols that involve the communication of certificates, and investigate some of the various logical and algorithmic questions that manifest during this endeavour.
Bio: Vaishnavi Sundararajan is an assistant professor in the department of computer science and engineering at IIT Delhi, where she is also associated with Center of Excellence in Cyber Systems and Information Assurance. She did her PhD at the Chennai Mathematical Institute and was at CNRS, Ericsson Research and University of California in Santa Cruz before joining IIT Delhi. Her research interests are broadly in formal methods and logic with a focus on applications to security.
