Murphi
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.
Homepage: http://verify.stanford.edu/dill/murphi.html
Additional examples (by Ulrich Stern): http://sprout.stanford.edu/uli/research.html
PRISM
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/
Homepage: http://www.cs.bham.ac.uk/~dxp/prism/index.html
Case studies: http://www.cs.bham.ac.uk/~dxp/prism/casestudies/index.html
MOCHA
Mocha is available on Leland System computers in the following directory: /usr/class/cs259/j-mocha/
Homepage: http://www-cad.eecs.berkeley.edu/~mocha/
OFMC
A model checker developed specifically for security protocol analysis.
Link to paper: http://www.avispa-project.org/papers/ofmc-esorics03.pdf
Link to home page: http://www.avispa-project.org
Constraint solver using prolog
Homepage: http://www.csl.sri.com/users/millen/capsl/constraints.html
Isabelle
Isabelle is a theorem proving environment developed at Cambridge University and TU Munich.
Homepage: http://www.cl.cam.ac.uk/Research/HVG/Isabelle/
Examples: http://www.cl.cam.ac.uk/users/lcp/papers/protocols.html
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:
|
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 |