scyther-proof
Version 0.3.1 revision 0 uploaded by SimonMeier.
Package meta
- Synopsis
- Automatic generation of Isabelle/HOL correctness proofs for security protocols.
- Description
scyther-proof is a security protocol verification tool based on an algorithm similar to the Scyther tool developed by Cas Cremers (http://people.inf.ethz.ch/cremersc/scyther/index.html). The theory underlying scyther-proof is described in the paper "Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs" by Meier, Cremers, and Basin available from http://people.inf.ethz.ch/meiersi/publications/index.html
Parts of the infrastructure underlying scyther-proof are reused in other projects by the same author. Therefore, most of its modules are exported in the corresponding scyther-proof library. However, this library is not yet thought for general use. Please contact the author, if you would like to build upon/extend scyther-proof.
- Author
- Simon Meier <simon.meier@inf.ethz.ch>
- Bug reports
- n/a
- Category
- Security, Theorem Provers
- Copyright
- Simon Meier, ETH Zurich, 2009-2011
- Homepage
- http://www.infsec.ethz.ch/people/meiersi/
- Maintainer
- Simon Meier <simon.meier@inf.ethz.ch>
- Package URL
- n/a
- Stability
- Beta