Home
Course description
Syllabus
Projects
Lecture slides
Tools and reference | |
Tools and Approaches
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/
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
 | 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 |
| 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 |
| 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 |
|
