scyther-proof-0.3.0: scyther-proof.cabal
build-type: Simple
name: scyther-proof
version: 0.3.0
license: GPL
license-file: LICENSE
category: Security, Theorem Provers
author: Simon Meier <simon.meier@inf.ethz.ch>
maintainer: Simon Meier <simon.meier@inf.ethz.ch>
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