This course is an introduction to analysis of security protocols. The course will cover a variety of contemporary security protocols and give students hands-on experience in using automated tools and formal techniques 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.
Grading Policy: There is no Final or Midterm exam for this course. Being a project centric course, we intend to weigh the course deliverables as follows:
20% - two homework assignments
30% - project proposal and progress reports
50% - project results and final report
Tentative Syllabus
Introduction to security protocols
 | Basic principles [1 lecture] | ||||||||
| Cryptographic background: [1 lecture] | ||||||||
| Security properties and attacks on them: [2 lectures]
| ||||||||
| Potential project topics [1 lecture] |
Formal analysis techniques
| Selection of projects |
| Finite-state model checking (Murphi) [3 lectures] |
| Constraint solving (SRI constraint solver) [1 lecture] |
| Process algebras (spi-calculus) [1 lecture] |
| Protocol logics (DDMP,Paulson) [2 lectures] |
| Probabilistic model checking (PRISM) [1/2 lecture] |
| Game theory (MOCHA: Kremer-Raskin examples) [1/2 lecture] |
| Equational proof system and probabilistic poly time [1 lecture] |
Project presentations [15 teams; 6 lectures]