Alladi Ramakrishnan Hall

Formal verification for security protocols

Vaishnavi Sundararajan

University of California Santa Cruz

Security protocols have become a permanent fixture of our highly-online lives today, and thus, it becomes paramount to ensure that they behave as intended. While the underlying cryptographic operations might not admit attacks, logical flaws in the protocol design might lead to catastrophic consequences. This is where formal verification has proved to be a handy tool for many decades. In this talk, we will see various models using which security protocols can be formally verified, starting from the now-standard Dolev-Yao model. We will present an extension to this model with “assertions”, which are first-order formulas that capture certification, and discuss algorithms for deciding security properties of interest. We will also briefly touch upon another model based on the logic FLAFOL for modelling and verifying protocols involving access control and delegation.