Formal Analysis of Secuirty Protocols

T 5-7pm, 719 Broadway, Room 709

Instructors:  Amir Pnueli (amir@cs.nyu.edu) and Lenore Zuck (zuck@cs.nyu.edu)

Office hours:  T 3-5 or by appointment

The class will be run as a combination of lectures and research seminar. It is intended mainly for students interested in security protocols and in formal methods. The course will focus on:

  1. Introduction to Security Protocols
  2. The Dolev-Yao Model, Models for Analysis of Security Protocols (e.g., Strand Spaces and Concrete Security)
  3. Temporal Approach to Analysis of Security Protocls
There is no textbook. Since most of the material in the lectures is not covered in textbooks, students are encourages to attend practically every class. Course work will entail reading material and assignments. The grade will be based on (3-5) assignments/mini-projects that may include class presentation of a research paper (chosen by the instructors.)

Prerequisites: Fundamental Algorithms and solid background in deductive methods and logics.


Lecture Notes

TLV Resources


  • Assignment 2 -- Specified in last page of Lecture6.
  • Miscellaneous