Formal Verification of Security Protocols

Nowadays, we use smart devices and the internet to do everything from chatting with friends to booking movie tickets to transferring large amounts of money to each other. How does one ensure that these cryptographic mechanisms (often called "security protocols") are secure (“nobody but me should be able to access my bank account”), private (“nobody should be able to link a payment from my anonymous Ethereum wallet to my real life identity”) etc?

It has been shown that even if the underlying cryptographic mechanisms are assumed to be perfectly correct, security protocols can often admit very problematic logical flaws. Attacks have been demonstrated on critical protocols ranging from those used for e-voting to those used in RFID passports. To get guarantees about safe operation, one can use formal verification, in which we mathematically model these protocols and the desired properties, and see if the model satisfies these properties. In this course, we will study how to formally model security protocols using various abstract systems, and how to express and verify properties over such models. In addition, since verification by hand is cumbersome and often error-prone, we will see how to code up protocols and verify properties using some specialized software.

We will also see how this analysis, which is based mostly in abstract logic and theoretical computer science, fits into the engineering workflow of a protocol going from design to deployment, and what challenges arise during this process. While this course concentrates on the formal analysis and verification of security protocols, many of the techniques used here provide a good introduction to the field of formal verification as a whole.

This course is for you if

• you have ever wondered how messaging systems like Signal or Whatsapp ensure that messages are "end-to-end encrypted", or

• you worry about whether banking systems really are as secure and correct as one would hope and expect, or

• you just have an interest in combining abstract tools like logic and automata theory with programming to solve real life problems.

The course involves concepts from automata theory, algorithms, logic, proof theory, and programming languages. Understanding the material will, therefore, require some mathematical acumen -- students should, at the very least, be able to write and understand rigorous formal proofs, especially those involving induction. Students will also be required to be conversant with basic concepts of syntax/semantics, automata, and algorithms. A very basic idea of logic and of complexity theory is also necessary; notions like inference, reductions, and NP-completeness should not seem unfamiliar. You should have taken the following courses at IIT Delhi:

• COL202 (Discrete Mathematical Structures), and

• COL352 (Introduction to Automata & Theory of Computation).

These courses are not a hard prerequisite. If you do not fulfil the above prerequisites, but think you have the necessary background to attend this course, feel free to get in touch.

• In-class quizzes: 10%
• Assignments: 40%
• Project/Paper presentation: 50%

Audit policy: 40% pass.