Logical explorations for security theory by Prof. Vaishnavi Sundararajan

Venue: Bharti 501

Abstract: Logics and proof theories play a large role in the formal study and analysis of systems, especially for formal verification. The exact shape of the syntax and proof 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 thissystem 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.