scyther-proof-0.3.1: scyther-proof.cabal
build-type: Simple
name: scyther-proof
version: 0.3.1
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 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.
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
CHANGES
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