build-type: Simple name: scyther-proof version: 0.3.0 license: GPL license-file: LICENSE category: Security, Theorem Provers author: Simon Meier maintainer: Simon Meier copyright: Simon Meier, ETH Zurich, 2009-2011 synopsis: Automatic generation of Isabelle/HOL correctness proofs for security protocols. description: scyther-proof is a security protocol verification tool based on a similar algorithm as 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. 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. homepage: http://www.infsec.ethz.ch/people/meiersi/ stability: Beta cabal-version: >= 1.8 data-dir: data data-files: HTML_TEMPLATE index.html js/jquery.js js/ui/jquery.ui.core.js js/ui/jquery.ui.widget.js js/ui/jquery.ui.tabs.js js/ui/jquery.ui.mouse.js js/ui/jquery.ui.draggable.js js/ui/jquery.effects.core.js js/jquery.layout.js js/tooltip/jquery.tooltip.css js/tooltip/lib/jquery.bgiframe.js js/tooltip/lib/jquery.dimensions.js js/tooltip/jquery.tooltip.js js/json_parse.js css/scyther-proof.css css/ui-lightness/jquery.ui.all.css css/ui-lightness/jquery.ui.button.css css/ui-lightness/jquery.ui.dialog.css css/ui-lightness/jquery.ui.selectable.css css/ui-lightness/jquery.ui.theme.css css/ui-lightness/jquery-ui-1.8.2.custom.css css/ui-lightness/jquery.ui.autocomplete.css css/ui-lightness/jquery.ui.core.css css/ui-lightness/jquery.ui.progressbar.css css/ui-lightness/jquery.ui.slider.css css/ui-lightness/jquery.ui.accordion.css css/ui-lightness/jquery.ui.base.css css/ui-lightness/jquery.ui.datepicker.css css/ui-lightness/jquery.ui.resizable.css css/ui-lightness/jquery.ui.tabs.css css/ui-lightness/images/ui-anim_basic_16x16.gif css/ui-lightness/images/ui-bg_flat_10_000000_40x100.png css/ui-lightness/images/ui-bg_glass_65_ffffff_1x400.png css/ui-lightness/images/ui-bg_highlight-soft_75_ffe45c_1x100.png css/ui-lightness/images/ui-icons_ef8c08_256x240.png css/ui-lightness/images/ui-bg_diagonals-thick_18_b81900_40x40.png css/ui-lightness/images/ui-bg_glass_100_f6f6f6_1x400.png css/ui-lightness/images/ui-bg_gloss-wave_35_f6a828_500x100.png css/ui-lightness/images/ui-icons_222222_256x240.png css/ui-lightness/images/ui-icons_ffd27a_256x240.png css/ui-lightness/images/ui-bg_diagonals-thick_20_666666_40x40.png css/ui-lightness/images/ui-bg_glass_100_fdf5ce_1x400.png css/ui-lightness/images/ui-bg_highlight-soft_100_eeeeee_1x100.png css/ui-lightness/images/ui-icons_228ef1_256x240.png css/ui-lightness/images/ui-icons_ffffff_256x240.png examples/OVERVIEW examples/Makefile examples/classic/*.spthy examples/iso9798/*.spthy examples/iso9798/isabelle-proofs/*.thy examples/iso9798/isabelle-parallel-proofs/*.thy isabelle/AUTHORS isabelle/document/root.tex isabelle/IsaMakefile isabelle/Makefile isabelle/README isabelle/ROOT.ML isabelle/src/isar-keywords.el isabelle/src/*.thy isabelle/src/ESPLogic/*.thy isabelle/src/ESPLogic/*.ML isabelle/src/compromising_adversaries/*.thy extra-source-files: .ghci interactive-only-src/Paths_scyther_proof.hs README flag threaded default: True description: Build with support for multithreaded execution library build-depends: base == 4.* , array == 0.3.* , containers >= 0.3 && < 0.5 , safe >= 0.2 && < 0.3 , mtl == 2.0.* , filepath >= 1.1 && < 1.3 , directory >= 1.0 && < 1.2 , process == 1.0.* , time >= 1.1 && < 1.3 , parsec == 3.1.* , pretty == 1.0.* , tagsoup == 0.12.* , json == 0.4.* , uniplate == 1.6.* build-tools: alex extensions: MultiParamTypeClasses, GeneralizedNewtypeDeriving hs-source-dirs: src exposed-modules: Extension.Prelude Data.Color Data.Table Data.DAG.Simple Data.UnionFind Control.Basics Control.Monad.BoundedDFS Control.Monad.Label Control.Concurrent.ManagedThreads Text.Isar Text.Dot Text.PrettyPrint.Class System.Isabelle System.Timing Scyther.Protocol Scyther.Message Scyther.Equalities Scyther.Event Scyther.Typing Scyther.Formula Scyther.Facts Scyther.Sequent Scyther.Proof Scyther.Theory Scyther.Theory.Lexer Scyther.Theory.Parser Scyther.Theory.Pretty Scyther.Theory.Html Scyther.Theory.Dot executable scyther-proof build-depends: base == 4.* , array == 0.3.* , containers >= 0.3 && < 0.5 , safe >= 0.2 && < 0.4 , mtl == 2.0.* , cmdargs >= 0.6.8 && < 0.7 , filepath >= 1.1 && < 1.3 , directory >= 1.0 && < 1.2 , process == 1.0.* , time >= 1.1 && < 1.3 , parsec == 3.1.* , pretty == 1.0.* , tagsoup == 0.12.* , json == 0.4.* , uniplate == 1.6.* if flag(threaded) ghc-options: -threaded main-is: Main.hs hs-source-dirs: src other-modules: Extension.Prelude Data.Color Data.Table Data.DAG.Simple Data.UnionFind Control.Basics Control.Monad.BoundedDFS Control.Monad.Label Control.Concurrent.ManagedThreads Text.Isar Text.Dot Text.PrettyPrint.Class System.Isabelle System.Timing Scyther.Protocol Scyther.Message Scyther.Equalities Scyther.Event Scyther.Typing Scyther.Formula Scyther.Facts Scyther.Sequent Scyther.Proof Scyther.Theory Scyther.Theory.Lexer Scyther.Theory.Parser Scyther.Theory.Pretty Scyther.Theory.Html Scyther.Theory.Dot Scyther.GoalFlow