CS259: Security Analysis of Network Protocols

Winter 2007-08

Class Location: Skilling 193 [map link]

Class Timings: Tuesdays and Thursdays, 2:15-3:30PM

Office Hours: TBD, Gates 476

Course Assistant: Arnab Roy

Office Hours: 5:30-6:30PM Tuesdays and 4-5:30PM Thursdays, Gates 490

Course Description:

The course will cover a variety of contemporary network protocols and give students hands-on experience in using automated tools or other techniques to analyze and evaluate security mechanisms. To understand security properties and requirements, we will look at several current protocols and their properties, including secrecy, authentication, key establishment, and fairness. In parallel, the course will look at several models and tools used in security analysis and examine 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, game theory, and executable models based on logic programming.

Individually or in small teams, students will select a protocol or system to analyze, identify 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. Projects may look at network protocols, or other kinds of systems, such as privacy systems, web security, and trusted computing architectures.

Lectures and Resources

Student Projects

Announcements:

· 2/5/08 – Graded homework 1 handed out in class.

· 2/1/08 – Homework 2 is out, due on 2/12/08. This is to get you started on using PRISM. The files you will need are: nw.pm and nw.pctl.

· Reminder – Project presentation #1 due on 1/31/08. Please prepare 1-2 slides on your project topic and send it to us by Thursday 12noon.

· 1/17/08 – Third problem added to Homework 1.

· 1/10/08 – Homework 1 is out, due on 1/24/08. There are two questions for now which will help you get started on Murphi. We will add 1-2 more questions soon. It is imperative that you have a working system by the time you get to the additional questions. There are clear instructions in the homework about how to run Murphi on Leland systems. Since Murphi can be intensely resource consuming sometimes, it is advisable to use Elaine machines. If you want to run Murphi elsewhere, please refer here. Talk to us if you still have practical problems running Murphi.

Resources from current students:

Many of the projects this year used Murphi as a model checking tool. Ilya Pirkin, a student of CS259 this year, has done a great job on correctness analysis of Ricart-Agrawala distributed mutual exclusion algorithm and its variants using Murphi. Sources and docs can be found here: [Link].

Resources from past offerings of the course:

· Winter 2006 Syllabus

· Winter 2006 Lecture Slides

· Winter 2004 Projects

· Winter 2006 Projects

· Winter 2006 Home Work 1,

· Winter 2006 Home Work 2a, Solutions

· Tools and References