Instructor: Daniele Micciancio
Time & Room: Tu/Th 12:30-1:50 (SSB 106)
This course is an introduction to the symbolic analysis of security protocols, and the interplay between symbolic and computational approaches to cryptography. The course will be mostly focused on the modeling of cryptographic operations and security properties, but will also give the students hands-on experience in using automated tools to analyze and evaluate cryptographic protocols. Specific topics covered in the course are:
The course is expected to be of interest for students in a variety of areas, including cryptography, computational complexity, computer and network security, logic, programming languages.
Prerequisites for the course are computatinal complexity (CSE200), and an introductory cryptography course (CSE207, but CSE107 is probably fine too.) If you are interested in the course, but are not sure about the prerequisites, come to the first lecture, and if still unsure, talk to the instructor.
Each lecture I will assign some papers to read. All students taking the class are expected to read the assigned papers before the following lecture, so that they can engage in active discussion during class. Below is a summary of the topics covered in class, lecture by lecture, together with the assignments for the next class and other homeworks.
March 29: Introduction to cryptography & course overview.
The material covered in the first lecture is mostly a review of prerequisites for this course. A good reference for background material on computational cryptography are Mihir Bellare and Phil Rogaway's lecture notes.
Reading assignments for next time:
March 31: The early days of public key cryptography.
There is a first homework assignment. Since many students have asked for an extension for various reasons, the deadline to submit the assignment has been moved to Thursday April the 14th for everybody. The homework is intended mostly to evaluate your cryptography background and/or ability to study on your own. The goal is to help you determine whether you should take this course for letter grade, or you are better off taking it with pass/fail option. You are allowed to consult lecture notes from other courses, reference books, the web, etc., as long as you clearly understand anything you write as part of your solution.
Next time we will talk about cryptographic protocols. Reading assignments for next lecture:
April 5 & 7: Cryptographic protocols
Reading assignments for the next 2 lectures:
April 12 & 14: The Dolev-Yao model
In these lectures we covered the symbolic model for security protocol proposed by Dolev and Yao, and the efficient algorithm for security analysis of Dolev, Even and Karp. In the next lecture we will cover some computational issues related to the Dolev-Yao model:
These issues are covered in the papers by Even and Goldreich, and Even, Goldreich and Shamir.
April 19: Dolev-Yao model and computational issues
In the next lectures we will start exploring automated tools for the verification of security protocols. We will start with Murphi, a model checker developed at Stanford that incorporate symmetry reduction and other techniques to improve the efficiency of the state space exploration, and allow to analyze larger systems. You can find the Murphi model checker at http://verify.stanford.edu/dill/murphi.html. You should try to install and test Murphi on your comptuer before the next lecture. Here are some personal installation notes. They may or may not apply to your specific computer platform. Refer to the main distribution page for general instructions.
April 21-26: Model checking
Reading assignment for April 26:
The first paper describes the application of Murphi to the analysis of three relatively simple authentication protocols, and it is a good introduction to the subject. The second paper is an example of applicability of Murphi to the analysis of more complex security properties.
Once you are familiar with Murphi, you can start working on the second homework assignment, due on May 5.
If you want to read more about using Murphi in the analysis of large security protocols, here are the pointers to two more papers:
April 28: Term rewriting and theorem proving.
You can download the casrul compiler and daTac theorem prover from the casrul webpage. Reading:
May 3-10: Computationally sound symbolic encryption
Reading:
Other related papers are:
May 12: Applications to secure database publishing
Reading:
May 17-19: Soundness of symbolic encryption with respect to active adversaries
Reading:
May 24-26: Applications to secure multicast key distribution, soundness of symbolic analysis and lower bounds.
Reading:
May 31-June 2: Other formal approaches: BAN logic, Spi-calculus, etc.
Reading:
Other related papers: