Syllabus

 

Home
Course description
Syllabus
Projects
Lecture slides
Tools and reference

Introduction to security protocols

Introduction: Course outline, Computer security, Cryptographic protocols, Security analysis, Needham-Schroeder example, Murphi

Lecture slides: ppt, pdf
Readings:
A Survey of Authentication Protocol Literature: Version 1.0, John Clark, Jeremy Jacob
Security Protocol Open Repository

 

SSL/TLS Case Study: Starting with the RFC describing the protocol, how to create an abstract model and code it up in Murphi, specify security properties, and run Murphi to check whether security properties are satisfied

Lecture slides: ppt, pdf
Readings:
Finite-State Analysis of SSL 3.0, John Mitchell, Vitaly Shmatikov, Ulrich Stern

 

Key Exchange Protocols: Key management, Kerberos, Public-Key infrastructure, Security properties and attacks on them, Needham-Schroeder Lowe protocol, Diffie-Hellman key exchange, IPsec, IKE

Lecture slides: ppt, pdf

 

Formal analysis techniques

Experiences in the Formal Analysis of the GDOI protocol (guest lecture by Catherine Meadows): Group Domain of Interpretation (GDOI) protocol, NRL Protocol Analyzer, NPATRL temporal requirements language,  Analysis of GDOI Using NPA/NPATRL, Logic for protocol analysis

Lecture slides: ppt, pdf

 

Contract-Signing Protocols: Fundamental limitation of Contract-Signing and Fair-Exchange, Trusted third party, Optimistic Contract-Signing, Asokan-Shoup-Waidner protocol, Desirable properties (fairness, timeliness, accountability, balance), Abuse-Free Contract-Signing

Lecture slides: ppt, pdf
Readings:
Optimistic Protocols for Fair Exchange, N. Asokan, Matthias Schunter, Michael Waidner
Abuse-free Optimistic Contract Signing, Juan Garay, Markus Jakobsson, Philip MacKenzie
Finite-State Analysis of Two Contract Signing Protocols, Vitaly Shmatikov, John Mitchell

 

Protocols for Anonymity: Applications of anonymity, Chaumís MIX, Dining Cryptographers, Anonymity via random routing (Onion Routing, Crowds System)

Lecture slides: ppt, pdf
Readings:
Untraceable Electronic Mail, Return addresses, and Digital Pseudonyms, David Chaum
Free Haven Project Anonymity Bibliography
The Cypherpunks Home Page

 

Probabilistic Model Checking: Crowds System, Probabilistic notions of anonymity, Markov  chains, PRISM, PCTL logic, Probabilistic fair exchange

Lecture slides: ppt, pdf
Readings:
Crowds: Anonymity for Web Transactions, Michael Reiter, Aviel Rubin
Automatic Verification of Real-Time Systems with Discrete Probability Distributions, Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston
Probabilistic Model Checking of an Anonymity System, Vitaly Shmatikov
PRISM Home Page

 

Protocol Verification by the Inductive Method: Protocol analysis using theorem proving, Inductive proofs, Isabelle theorem prover, Verifying the Secure Electronic Transactions (SET) protocols using Isabelle

Lecture slides: ppt, pdf
Readings:
The Inductive Approach to Verifying Cryptographic Protocols, Lawrence Paulson
Verifying Security Protocols Using Isabelle, a collection of case studies
Collection of Epayment protocols

 

Probabilistic Contract Signing: Rabinís Beacon, Rabinís Contract Signing protocol, BGMR probabilistic Contract Signing, Formal model for the BGMR protocol

Lecture slides: ppt, pdf
Readings:
A Fair Protocol for Signing Contracts, Michael Ben-Or, Oded Goldreich, Silvio Micali, Ronald Rivest
Analysis of Probabilistic Contract Signing, Gethin Norman, Vitaly Shmatikov

 

Logic for Computer Security Protocols: Floyd-Hoare logic of programs, BAN Logic, Compositional Logic for Proving Security Properties of Protocols

Lecture slides (part 1): ppt, pdf
Lecture slides (part 2): ppt, pdf
Readings:
A Logic of Authentication, Michael Burrows, Martin Abadi, Roger Needham
A Compositional Logic for Proving Security Properties of Protocols, Nancy Durgin, John Mitchell, Dusko Pavlovic
A Derivation System for Security Protocols and its Logical Formalization, Anupam Datta, Ante Derek, John Mitchell, Dusko Pavlovic

 

Symbolic Protocol Analysis: Strand space model, Symbolic analysis problem, From protocols to constraints, SRI Constraint Solver

Lecture slides: ppt, pdf
Readings:
Strand Spaces: Why is a Security Protocol Correct?, Joshua Guttman, Jonathan Herzog, Javier Thayer
Constraint Solving for Bounded-Process Cryptographic Protocol Analysis, Jonathan Millen, Vitaly Shmatikov
Constraint Solving in Prolog

 

Security in Process Calculus: Pi Calculus, Modeling secrecy with scoping, Applied Pi Calculus, Security as observational equivalence, Testing equivalence

Lecture slides: ppt, pdf
Readings:
A Calculus for Cryptographic Protocols: The Spi Calculus, Martin Abadi, Andrew Gordon
Mobile Values, new Names, and Secure Communication, Martin Abadi, Cedric Fournet
Reconciling Two Views of Cryptography, Martin Abadi, Phillip Rogaway

 

Game-Based Verification of Fair Exchange Protocols: The problem of fair exchange, Protocol as a game tree, Alternating transition systems, Alternating-time temporal logic, MOCHA Model Checker

Lecture slides: ppt, pdf
Readings:
Alternating-time Temporal Logic, Rajeev Alur, Thomas Henzinger, Orna Kupferman
Mocha: Modularity in Model Checking, Rajeev Alur, Thomas Henzinger, F.Y.C. Mang, Shaz Qadeer, Sriram Rajamani, Serdar Tasiran
A Game-Based Verification of Non-Repudiation and Fair Exchange Protocols, Steve Kremer, Jean-Francois Raskin
Game Analysis of Abuse-free Contract Signing, Steve Kremer, Jean-Francois Raskin

 

Probabilistic Polynomial-Time Process Calculus for Security Protocol Analysis: Equivalence-based specification of correctness, Probabilistic poly-time analysis, Security of encryption schemes, Process calculus, Probabilistic observational equivalence

Lecture slides: ppt, pdf
Readings:
A Probabilistic Polynomial-Time Calculus for Analysis of Cryptographic Protocols, John Mitchell, Ajith Ramanathan, Andre Scedrov, Vanessa Teague
A Bisimulation Method for Cryptographic Protocols, Martin Abadi, Andrew Gordon

Project Presentations

iKP: i-Key-Protocol (Secure Electronic Payment), Christopher Hsu
Analysis of an Internet Voting Protocol, Dale Neal, Garrett Smith
XML Security, Jun Yoshida
 

Last updated: March 03, 2004.