Analyzing how secure a system is usually falls into one of two categories: analyzing the correctness of security mechanisms (e.g., authentication protocols such as Kerberos), and analyzing the correctness of the implementation of security mechanisms (e.g., an application implementing Kerberos for authentication). Clearly, correctness of mechanism is a prerequisite to correctness of implementation. In some sense, it is useless to verify that a program is correctly implemented if the mechanism that the program is supposed to implement is already broken.

The purpose of this course is to survey modern methods for reasoning about the correctness of security mechanisms, with an eye towards automatic validation. The goal is to bring students to the level of being able to read current literature in the field. Topics to be covered will depend on time and interests, and will include:

  • symbolic analysis of security protocols
  • access control mechanisms
  • trust management
  • information flow
  • automatic validation and cryptography

The course will consist of standard lectures as well as student presentations of both classic and recent research papers. Techniques will borrow heavily from logic, model checking, theorem proving, programming language semantics, and type systems---exactly which we will focus on will depend on student backgrounds.

Who:   Riccardo Pucella
328 West Village H
Office Hours: Thu 15h00-17h00
When: Thu 18h00-21h00
Where: 236 Forsyth



Apr 28: That's it! Thanks everyone for your patience in the final weeks, and have a great summer.

Apr 5: The preliminary schedule for student presentations is below. I will try to add links to the corresponding papers, so that people can have a look at them in advance.

Mar 24: Richard points me to Tor, an anonymizing framework based on onion routing, something that seems to scale better than crowds.

Mar 23: Papers for next lecture (march 30) are below, on policies.

Mar 19: I completely forgot about the papers for next lecture. I apologize about that. The lecture will be on anonymity; the papers are below. They should be an easy-ish read.

Mar 7: I have posted the notes on BAN logic below. I have also posted the papers for next lecture.

Feb 24: Readings for next class posted. Also, here is the promised writeup on the project, including suggestions.

Feb 23: Lecture notes for tonight's lecture are available. Later tonight, I will be posting some suggestions for projects, as well as the reading for next class.

Feb 19: Paper for next lecture is available; I apologize for the delay, but it took me a while to find the version I wanted. I have also posted (sometimes rough) lecture notes for previous lectures.

Feb 2: The paper for Feb 9 lecture is available; only one this time, to make up for the fact that there were three last time...

Jan 26: Papers for Feb 2 lecture are available.

Jan 24: Last class, I mentioned that I would be posting some papers to read for next class. For a variety of reasons, not the least of which being that some of those papers are not freely available online, I will distribute them in class instead.




Course Information


Course Staff

Instructor:   Riccardo Pucella
328 West Village H
Office Hours: Thu 15h00-17h00
Teaching Assistant: In my dreams...



No formal prerequisites. But I will shamelessly assume some mathematical maturity, and the ability to read research papers.



I expect every student to give an hour presentation based on 2 or 3 papers from the literature, on a subject of interest to him or her that falls under the scope of the course subject. The grade will be based on that presentation.



No textbooks. I will distribute papers from the literature for readings, and prepare handouts when relevant.



Schedule and Lecture Notes

Here is a list of the lectures planned for the course. Note that this schedule is subject to change.

I have given for every lecture the readings that should be done for that lecture. Papers that are not available online will be distributed in class.

Jan 12 Introduction
Jan 19 Security protocols; Message secrecy
- Notes
Jan 26 Authentication; Correspondence assertions
- D. Gollmanm, What do we mean by entity authentication?
- T. Woo, S. Lam, A semantic model for authentication protocols
Feb 2 CSP and model checking
- P. Ryan, S. Schneider, An introduction to CSP
- G. Lowe, Breaking and fixing the Needham-Schroeder public-key protocol using FDR
- G. Lowe, A hierarchy of authentication specifications
Feb 16 Theorem proving
- L. Paulson, The inductive approach to verifying cryptographic protocols
- The protocol verification page for Isabelle
- Notes
Feb 23 The spi calculus
- M. Abadi, A. Gordon, A calculus for cryptographic protocols: the spi calculus [in pdf]
- Notes
Mar 2 BAN logic
- M. Burrows, M. Abadi, R. Needham, A Logic of Authentication
- M. Abadi, M. Tuttle, A Semantics for a Logic of Authentication
- Notes
Mar 9 Spring Break - no classes
Mar 16 Information flow
- H. Mantel, Possibilistic Definitions of Security - An Assembly Kit
- A. Sabelfeld, A. Myers, Language-Based Information-Flow Security
Mar 23 Anonymity
- M. Reiter, A. Rubin, Crowds: Anonymity for Web Transactions
- J. Halpern, K. O'Neill, Anonymity and Information Hiding in Multiagent Systems
Mar 29 Policies
- R. van der Meyden, The Dynamic Logic of Permission
- J. Halpern, V. Weissman, Using First-Order Logic to Reason about Policies
Apr 6 Presentations
Joan Paul: A cost-based framework for analyzing denial of service
Therapon Skotiniotis: Generation and evaluation of NIDS attacks
Apr 13 Presentations
Richard Conlan: Cassandra and Datalog
Vassilis Koutavas: Types systems for authentication
Ryan Culpepper: Strand spaces
Apr 20 Presentations
Wendy Minton: Braid-based cryptographic protocols
James Wexler: Constraint satisfaction for protocol analysis
Jingsong Feng: Model Checking Protocols
Dale Vaillancourt: ProVerif
Apr 27 Presentations
Zach Kissel: Access control and trust management
Ignacio Marin-Garcia: Cyberforensics
Rahul Gera: Enforceable security policies
Sam Tobin-Hochstadt: