build-type:         Simple
name:               scyther-proof
version:            0.10.0.1
license:            GPL
license-file:       LICENSE
category:           Security, Theorem Provers
author:             Simon Meier <iridcode@gmail.com>, 
                    Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
maintainer:         Simon Meier <iridcode@gmail.com>
copyright:          Simon Meier, Andreas Lochbihler, ETH Zurich, 2009-2013

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
                    2013 Journal of Computer Security paper 
                    \"Efficient Construction of 
                    Machine-Checked Protocol Security Proofs\" 
                    by Meier, Cremers, and Basin available from
                    <https://github.com/meiersi/scyther-proof/tree/master/publications>.
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/Makefile
  isabelle/README
  isabelle/ROOT
  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
  README.md
  CHANGES


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

executable scyther-proof
    build-depends:
        base          == 4.*    ,
        array         >= 0.3   && < 0.6 ,
        containers    >= 0.4.2 && < 0.6 ,
        safe          >= 0.2   && < 0.4 ,

        mtl           >= 2.1   && < 3.0,

        cmdargs       >= 0.10.7 ,
        filepath      >= 1.2   && < 1.5 ,
        directory     >= 1.0   && < 1.3 ,
        process       >= 1.1   && < 1.3 ,
        time          >= 1.1   && < 1.6 ,

        parsec        == 3.1.*  ,
        pretty        >= 1.0   && < 1.2 ,
        tagsoup       >= 0.12  && < 0.14 ,
        json          >= 0.5   && < 0.10 ,
        uniplate      == 1.6.* ,
        utf8-string   >= 0.3.7

    build-tools:
        alex          >= 3.0   && < 3.2

    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

source-repository head
  type:     git
  location: https://github.com/meiersi/scyther-proof.git