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 developed at the University of Birmingham and now based
at the Oxford University.
Homepage: http://www.prismmodelchecker.org/
Case studies: http://www.prismmodelchecker.org/casestudies/index.php
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/~lp15/papers/isabelle.html