scyther-proof-0.4.1.0: Automatic generation of Isabelle/HOL correctness proofs for security protocols.

The scyther-proof package

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

Properties

Versions0.3.0, 0.3.1, 0.4.0, 0.4.1.0
Dependenciesarray (≥0.3 & <0.5), base (4.*), cmdargs (≥0.6.8 & <0.7), containers (≥0.4.2 & <0.5), directory (≥1.0 & <1.3), filepath (≥1.2 & <1.4), json (0.5.*), mtl (2.0.*), parsec (3.1.*), pretty (≥1.0 & <1.2), process (1.1.*), safe (≥0.2 & <0.4), tagsoup (0.12.*), time (≥1.1 & <1.3), uniplate (1.6.*)
LicenseGPL
CopyrightSimon Meier, ETH Zurich, 2009-2011
AuthorSimon Meier <simon.meier@inf.ethz.ch>
MaintainerSimon Meier <simon.meier@inf.ethz.ch>
StabilityBeta
CategorySecurity, Theorem Provers
Home pagehttp://www.infsec.ethz.ch/people/meiersi/
Executablesscyther-proof
Upload dateMon May 14 07:42:42 UTC 2012
Uploaded bySimonMeier

Downloads