**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:

- Various classic examples of network security protocols
- Several standard formal models for security analysis, like Dolev-Yao model, BAN logic and derivatives, process algebras (e.g., the spi-calculus), and type theoretic approaches.
- A selection of tools for automated protocol analsis, including model checkers (e.g., Murphi), and theorem provers (Isabelle/HOL), and examples of their application to security analysis.
- Current work on bridging the gap between symbolic and computational analysis, and examples of computationally sound symbolic security analysis.

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:

- Diffie, Hellman,
*New directions in cryptography*, IEEE TIT 22(6):644-654 (1976) - Rivest , Shamir, Adleman,
*A method for obtaining digital signatures and public-key cryptosystems*, CACM 21(2):120-126 (1978)

**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:

- Needham, Schroeder.
*Using encryption for authentication in large networks of computers*, CACM 21(12):993-999 (1978) - Denning, Sacco,
*Timestamps in key distribution protocols*, CACM 24(8):533-536 (1981) - Otway, Rees.
*Efficient and timely mutual authentication*, OS Review 21(1):8-10 (1987)

**April 5 & 7:** Cryptographic protocols

Reading assignments for the next 2 lectures:

- Dolev, Yao,
*On the security of public key protocols*, IEEE TIT 29(2):198-208 (1983) - Dolev, Even, Karp,
*On the security of ping-pong protocols*, Inform.and Control 55:57-68 (1982) - Even, Goldreich,
*On the security of multi-party ping-pong protocols*, FOCS 1983: 34-39 - Even, Goldreich, Shamir,
*On the security of ping-pong protocols when implemented using the RSA*, CRYPTO 1985

**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:

- What does the Dolev-Yao model says about security of protocols implemented with typical encryption functions, like RSA, that satisfy homomorphic properties?
- Is security efficiently decidable even when we extend the model in various ways?

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:

*Automated analysis of cryptographic protocols using Murphi*, Mitchell, Mitchell, Stern (SSP 1997)*Finite-state analysis of two contract signing protocols*, Shmatikov, Mitchell, TCS 283(2):419-450, 2002

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:

*Finite-State Analysis of SSL 3.0*, Mitchell, Shmatikov, Stern (USENIX 1998)*Efficient Finite-State Analysis for Large Security Protocols,*Shmatikov, Stern (CSFW 1998)

**April 28:** Term rewriting and theorem proving.

You can download the casrul compiler and daTac theorem prover from the casrul webpage. Reading:

*Compiling and Verifying Security Protocols*, Jacquemard, Rusinowitch, Vigneron (LPAR 2000)

**May 3-10:** Computationally sound symbolic encryption

Reading:

- Abadi, Rogaway:
*Reconciling Two Views of Cryptography*. J. Cryptology 15(2): 103-127 (2002) - Micciancio, Warinschi:
*Completeness Theorems for the Abadi-Rogaway Language of Encrypted Expressions*. JCS 12(1): 99-130 (2004)

Other related papers are:

- Abadi, Jurjens:
*Formal Eavesdropping and Its Computational Interpretation*. TACS 2001: 82-94. (Full version.) - Horvitz, Gligor:
*Weak Key Authenticity and the Computational Completeness of Formal Encryption.*CRYPTO 2003: 530-547

**May 12:** Applications to secure database publishing

Reading:

- Abadi, Warinschi:
*Security Analysis of Cryptographically Controlled Access to XML Documents*, PODS 2005

**May 17-19:** Soundness of symbolic encryption with respect
to active adversaries

Reading:

- Micciancio, Warinschi:
*Soundness of formal encryption in the presence of active adversaries*. TCC 2004

**May 24-26:** Applications to secure multicast key
distribution, soundness of symbolic analysis and lower bounds.

Reading:

- Micciancio, Panjwani:
*Adaptive security of symbolic encryption.*TCC 2005 - Micciancio, Panjwani:
*Optimal communication complexity of generic multicast key distribution.*Eurocrypt 2004

**May 31-June 2:** Other formal approaches: BAN logic,
Spi-calculus, etc.

Reading:

- Burrows, Abadi, Needham,
*A logic of authentication*, ACM TOCS 8(1):18-36 (1990) - Abadi, Gordon,
*A Calculus for Cryptographic Protocols: The Spi Calculus*, I&C 148(1):1-70 (1999)

Other related papers:

- Abadi, Tuttle,
*A semantics for a logic of authentication*, PODC 1991 - Syverson, vanOorschot,
*On unifying some cryptographic protocol logics*, SSP 1994 - Dekker,
*C3PO: a tool for automatic sound cryptographic protocol analysis*, CSFW 2000 - Abadi,
*Secrecy by typing in security protocols*, JACM 46(5):749-786 (1999) - Abadi, Blanchet,
*Analyzing security protocols with secrecy types and logic programs*, JACM 52(1):102-146