This course is an introduction to analysis of security protocols. The course will cover a variety of contemporary network protocols and give students hands-on experience in using automated tools to analyze and evaluate cryptographic protocols and other security mechanisms. The first part of the course will survey protocols and their properties, including secrecy, authentication, key establishment, and fairness. The second part will cover standard formal models and tools used in security protocol analysis, and describe their advantages and limitations. In addition to fully automated finite-state model checking techniques, we will also study other approaches, such as constraint solving, process algebras, protocol logics, probabilistic model checking, and game theory. The third part of the course will consist of student presentations of term projects.

Individually or in small teams, students will select a protocol or system to analyze, describe the system and its desired properties in a precise way, and use one of the tools or methods covered in the course to perform a security analysis. A set of candidate systems will be given, but students may propose their own.

This course compliments CS 155, Introduction to Computer Security, and the cryptography courses, CS 255 and CS 355. A network protocol such as SSL (Secure Sockets Layer) may fail in three ways: the protocol design may be flawed, the cryptography may be inadequate, or the implementation may be buggy. CS 259 is concerned with protocol flaws, CS 255 with cryptography, and CS 155 with secure implementation.

Prerequisites: CS155 is recommended but not required. Prior understanding of network protocols is also helpful.

Important: CS 259 will satisfy the same degree requirements as CS 258, which will not be offered this year.

Tentative Syllabus

Introduction to security protocols

Formal analysis techniques

Project presentations [15 teams; 6 lectures]

Last updated: January 20, 2004.