Advanced Topics

Formal Methods and Security
We give a history of the application of formal methods to security. From there we follow several of the current threads in formal methods and security in more depth, including information flow models, analysis of cryptographic protocols, access control and trust management, and operating system security
Lecture Notes 1 | Lecture Notes 2
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video
Catherine Meadows

Cryptographic Protocols
Lecture Notes 1 | Lecture Notes 2
Lecture Notes 3 | Lecture Notes 4
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video | Lecture 4 Video
Cedric Fournet

Linear Logic and Security
Many proposed languages for specifying and analyzing security protocols are rooted in linear logic. In this course, we show how languages such as MSR, strand spaces, and the spi-calculus map to linear logic, and how this logical interpretation can be exploited to relate these languages and some of the reasoning methods they support best.
Course Materials
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video | Lecture 4 Video
Iliano Cervesato

Typed Assembly Language and Proof Carrying Code
Lecture Notes pdf | ps | powerpoint
Lecture 1 Video | Lecture 2 Video
David Walker

Language-Based Information-Flow Security
Lecture Notes ps | pdf
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video
Steve Zdancewic

Global Computing
Lecture Notes ps | pdf
Lecture 1 Video | Lecture 2 Video
Lecture 3 Video | Lecture 4 Video
Lecture 5 Video
Vladimiro Sassone