ACN910 / INF672: Protocol Verification and Safety

In this course, we will learn how to formally verify network protocols and their implementations for safety and security properties. We will learn to use automated tools like the Spin model checker, the Coq theorem prover, and the ProVerif crytpographic protocol analyzer and see how they can be used to analyze modern real-world network protocols like AODV and TLS 1.3.

Slides

Verification Tools

During the course, you will be expected to install and run various verification tools on your own laptops. If you find it difficult to install the tools directly on your machine, you may want to try this virtual machine image. To run it, you will need to download and install VirtualBox.