scyther-proof-0.4.0: scyther-proof.cabal

build-type:         Simple
name:               scyther-proof
version:            0.4.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 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
  examples/experimental/ExponentialBlowup.spthy

  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
  src/Scyther/Theory/Lexer.x_src_only
  README
  CHANGES


flag threaded
    default: True
    description: Build with support for multithreaded execution

executable scyther-proof
    build-depends:
        base          == 4.*    , 
        array         >= 0.3   && < 0.5 , 
        containers    >= 0.4.2 && < 0.5 ,
        safe          >= 0.2   && < 0.4 ,
                      
        mtl           == 2.0.*  ,
        
        cmdargs       >= 0.6.8 && < 0.7 ,
        filepath      >= 1.2   && < 1.4 ,
        directory     >= 1.0   && < 1.3 ,
        process       == 1.1.*  , 
        time          >= 1.1   && < 1.3 ,
        
        parsec        == 3.1.*  ,
        pretty        == 1.0.*  ,
        tagsoup       == 0.12.*  ,
        json          == 0.5.*  ,
        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