Tools
Murphi is a protocol description language verifier based on explicit state enumeration. It was developed in David Dill's research group.
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 is a probabilistic model checker being developed at the University of Birmingham.
Homepage: http://www.cs.bham.ac.uk/~dxp/prism/index.html
Case studies: http://www.cs.bham.ac.uk/~dxp/prism/casestudies/index.html
Homepage: http://www-cad.eecs.berkeley.edu/~mocha/
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
Homepage: http://www.csl.sri.com/users/millen/capsl/constraints.html
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