Tools and reference


Course description
Lecture slides
Tools and reference

Tools and Approaches


Murphi is a protocol description language verifier based on explicit state enumeration. It was developed in David Dill's research group.

Murphi  is available on Leland System computers in the following directory: /usr/class/cs259/Murphi3.1/

Problems have been reported with running the official version of Murphi on various systems. If it does not run properly on your machine try with this slightly modified version. If the problems persist, please contact the TA for assistance.  

Additional examples (by Ulrich Stern): 



PRISM is a probabilistic model checker being developed at the University of Birmingham.

PRISM is available on Leland System computers in the following directories: /usr/class/cs259/prism-solaris/ and /usr/class/cs259/prism-linux/

Case studies:



Mocha is available on Leland System computers in the following directory: /usr/class/cs259/j-mocha/



Constraint solver using prolog




Isabelle is a theorem proving environment developed at Cambridge University and TU Munich.



Reference materials

Collections on protocols analysis

A Survey of Authentication Protocol Literature: Version 1.0, John Clark, Jeremy Jacob
Security Protocol Open Repository

Background Reading on SSL 3.0

Analysis of the SSL 3.0 protocol, David Wagner, Bruce Schneier
Finite-State Analysis of SSL 3.0, John Mitchell, Vitaly Shmatikov, Ulrich Stern
Chosen Ciphertext Attacks against Protocols Based on RSA Encryption Standard PKCS #1, Daniel Bleichenbacher

RFCs and Internet-Drafts

RFC2246 - The TLS Protocol Version 1.0
Internet Key Exchange (IKEv2) Protocol
List of current RFCs can be found here
List of current Internet-Drafts can be found here

Contract signing protocols

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
A Fair Protocol for Signing Contracts, Michael Ben-Or, Oded Goldreich, Silvio Micali, Ronald Rivest
Analysis of Probabilistic Contract Signing, Gethin Norman, Vitaly Shmatikov

Protocols for Anonymity

Untraceable Electronic Mail, Return addresses, and Digital Pseudonyms, David Chaum
Free Haven Project Anonymity Bibliography
The Cypherpunks Home Page
Anonymity systems in various stages of deployment:
Zero-Knowledge Systems:

Probabilistic Model Checking

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

Protocol Verification by the Inductive Method

The Inductive Approach to Verifying Cryptographic Protocols, Lawrence Paulson
Verifying Security Protocols Using Isabelle, a collection of case studies

Logic for Computer Security Protocols

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

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

Game-Based Verification of Protocols

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


Last updated: February 27, 2004.