tamarin-prover.cabal

cabal-version:      >= 1.18
build-type:         Simple
name:               tamarin-prover
version:            0.9.0
license:            GPL
license-file:       LICENSE
category:           Theorem Provers
author:             Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>,
                    Simon Meier <simon.meier@inf.ethz.ch>,
                    Jannik Dreier <research@jannikdreier.net>,
                    Ralf Sasse <ralf.sasse@gmail.com>
maintainer:         Simon Meier <simon.meier@inf.ethz.ch>,
                    Jannik Dreier <research@jannikdreier.net>,
                    Ralf Sasse <ralf.sasse@gmail.com>
copyright:          Benedikt Schmidt, Simon Meier, Jannik Dreier, Ralf Sasse, ETH Zurich, 2010-2015
synopsis:           The Tamarin prover for security protocol analysis.
description:

    The Tamarin prover is a tool for the analysis of security protocols. It
    implements a constraint solving algorithm that supports both falsification
    and verification of security protocols with respect to an unbounded number
    of sessions. The underlying security protocol model uses multiset
    rewriting to specify protocols and adversary capabilities, a guarded
    fragment of first-order logic to specify security properties, and
    equational theories to model the algebraic properties of cryptographic
    operators.
    .
    The paper describing the theory underlying the Tamarin prover was
    accepted at CSF 2012. Its extended version is available from
    <http://tamarin-prover.github.io>.
    .
    The Tamarin prover supports both a batch analysis mode and the
    interactive construction of security proofs using a GUI. Example protocols
    and the user guide are installed together with the prover. Just call the
    @tamarin-prover@ executable without any arguments to get more information.
    .
    The Tamarin prover uses maude (<http://maude.cs.illinois.edu/>) as a
    unification backend and GraphViz (<http://www.graphviz.org/>) to visualize
    constraint systems. Detailed instructions for installing the Tamarin
    prover are given at <http://tamarin-prover.github.io>.
    .
    The paper describing the theory underlying the extension for observational
    equivalence is published at CCS 2015. Its extended version is available from 
    <http://tamarin-prover.github.io>. For observational equivalence proofs just 
    add the "--diff" flag when calling the @tamarin-prover@.

homepage:           http://tamarin-prover.github.io


--------------
-- extra files
--------------

extra-source-files:
  -- cached intruder variants for DH and BP
  data/intruder_variants_dh.spthy
  data/intruder_variants_bp.spthy

  -- files for the web-frontend
  data/img/*.ico
  data/img/*.gif
  data/img/*.png
  data/js/*.js
  data/css/*.css
  data/css/smoothness/*.css
  data/css/smoothness/images/*.png


-------------------------
-- repository information
-------------------------

source-repository head
  type:     git
  location: https://github.com/tamarin-prover/tamarin-prover.git

--------------
-- build flags
--------------

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

flag test-coverage
    default: True
    manual: True
    description: Build with test coverage support

flag build-tests
  default: False
  manual: True
  description: Build unit test driver


----------------------
-- executables stanzas
----------------------

executable tamarin-prover
    default-language: Haskell2010

    if flag(threaded)
        ghc-options:   -threaded -eventlog 
    
    -- -XFlexibleInstances
    -- Note that eager blackholing lead to segfaults: See GHC Ticket #6146
    -- Morevoer, it seems that the bug is not fully fixed on GHC 7.4.2, as we
    -- still get segfaults: see GHC Ticket #7076.
    -- Therefore, we do not use -feager-blackholing (yet).

    ghc-options:       -Wall -fwarn-tabs -rtsopts
    ghc-prof-options:  -auto-all

    -- Parallelize by default. Only activated for GHC 7.4, as this flag was
    -- unstable in earlier -- versions; i.e., it resulted in command-line
    -- parsing errors.
    if impl(ghc >= 7.4) && flag(threaded)
        ghc-options:   -with-rtsopts=-N

    hs-source-dirs:    src
    main-is:           Main.hs

    build-depends:
        HUnit
      , aeson
      , array
      , base
      , binary
      , blaze-builder
      , blaze-html
      , bytestring
      , bytestring
      , cmdargs
      , conduit
      , containers
      , deepseq
      , derive
      , directory
      , dlist
      , fclabels
      , file-embed
      , filepath
      , hamlet
      , http-types
      , lifted-base
      , monad-control
      , mtl
      , old-locale
      , parallel
      , parsec
      , process
      , resourcet
      , safe
      , shakespeare
      , syb
      , text
      , threads
      , time
      , transformers
      , uniplate
      , wai
      , warp
      , yesod-core
      , yesod-json
      , yesod-static

      , tamarin-prover-utils  == 0.9.0
      , tamarin-prover-term   == 0.9.0
      , tamarin-prover-theory == 0.9.0

    other-modules:
      Paths_tamarin_prover

      Main
      Main.Console
      Main.Environment
      Main.TheoryLoader
      Main.Utils
      Main.Mode.Batch
      Main.Mode.Interactive
      Main.Mode.Intruder
      Main.Mode.Test

      Web.Dispatch
      Web.Hamlet
      Web.Handler
      Web.Instances
      Web.Settings
      Web.Theory
      Web.Types

      Test.ParserTests