tamarin-prover-0.4.0.0: tamarin-prover.cabal
cabal-version: >= 1.8
build-type: Simple
name: tamarin-prover
version: 0.4.0.0
license: GPL
license-file: LICENSE
category: Theorem Provers
author: Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>,
Simon Meier <simon.meier@inf.ethz.ch>
maintainer: Simon Meier <simon.meier@inf.ethz.ch>
copyright: Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012
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://www.infsec.ethz.ch/research/software#TAMARIN>.
.
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.uiuc.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://www.infsec.ethz.ch/research/software#TAMARIN>.
homepage: http://www.infsec.ethz.ch/research/software#TAMARIN
--------------
-- extra files
--------------
data-dir: data
data-files:
LICENSE
AUTHORS
CHANGES
-- cached intruder variants for DH-exponentiation
intruder_variants_dh.spthy
-- files for the web-frontend
img/*.ico
img/*.gif
img/*.png
js/*.js
css/*.css
css/smoothness/*.css
css/smoothness/images/*.png
-- vim syntax highlighting
etc/spthy.vim
etc/filetype.vim
-- documentation
doc/MANUAL
-- example files
examples/stable/Tutorial.spthy
examples/stable/TLS.spthy
examples/stable/InvariantsExample.spthy
-- CSF'12 case studies
examples/csf12/Artificial.spthy
examples/csf12/DH2_original.spthy
examples/csf12/KAS1.spthy
examples/csf12/KAS2_eCK.spthy
examples/csf12/KAS2_original.spthy
examples/csf12/KEA_plus_KI_KCI.spthy
examples/csf12/KEA_plus_KI_KCI_wPFS.spthy
examples/csf12/KEA_plus_eCK.spthy
examples/csf12/NAXOS_eCK_PFS.spthy
examples/csf12/NAXOS_eCK.spthy
examples/csf12/UM_eCK.spthy
examples/csf12/UM_eCK_noKCI.spthy
examples/csf12/UM_PFS.spthy
examples/csf12/UM_wPFS.spthy
examples/csf12/UM_PFS.spthy
examples/csf12/SignedDH_PFS.spthy
examples/csf12/SignedDH_eCK.spthy
examples/csf12/STS_MAC.spthy
examples/csf12/STS_MAC_fix1.spthy
examples/csf12/STS_MAC_fix2.spthy
examples/csf12/JKL_TS1_2004_KI.spthy
examples/csf12/JKL_TS1_2008_KI.spthy
examples/csf12/JKL_TS2_2004_KI_wPFS.spthy
examples/csf12/JKL_TS2_2008_KI_wPFS.spthy
examples/csf12/JKL_TS3_2004_KI_wPFS.spthy_nonterm
examples/csf12/JKL_TS3_2008_KI_wPFS.spthy_nonterm
extra-source-files:
.ghci
interactive-only-src/Paths_tamarin_prover.hs
interactive-only-src/Lexer.x
--------------
-- build flags
--------------
flag no-gui
default: False
description: Do not build the web-application GUI.
flag threaded
default: True
description: Build with support for multithreaded execution
flag test-coverage
default: True
description: Build with test coverage support
flag build-tests
default: False
description: Build unit test driver
----------------------
-- executables stanzas
----------------------
executable tamarin-prover
if flag(threaded)
ghc-options: -threaded
ghc-options: -Wall -funbox-strict-fields -fwarn-tabs -rtsopts
ghc-prof-options: -auto-all
hs-source-dirs: src
main-is: Main.hs
if flag(no-gui)
cpp-options: -DNO_GUI
if !flag(no-gui)
-- To help the top-down solver we put the more difficult to solve yesod
-- dependencies up front.
build-depends:
bytestring == 0.9.*
, blaze-html == 0.4.*
, http-types == 0.6.*
, blaze-builder == 0.3.*
, yesod-core == 0.10.*
, yesod-json == 0.3.*
, yesod-static == 0.10.*
-- , yesod-form == 0.4.* -- required once we reactivate editing
, text == 0.11.*
, wai == 1.1.*
, hamlet == 0.10.*
, warp == 1.1.*
, aeson == 0.6.*
, old-locale == 1.0.*
, monad-control == 0.3.*
, lifted-base
, threads == 0.4.*
build-depends:
base == 4.*
, bytestring == 0.9.*
, deepseq == 1.3.*
, array >= 0.3 && < 0.5
, containers >= 0.4.2 && < 0.5
, mtl == 2.0.*
, cmdargs == 0.9.*
, filepath >= 1.1 && < 1.4
, directory >= 1.0 && < 1.2
, process == 1.1.*
, parsec == 3.1.*
, safe >= 0.2 && < 0.4
, transformers == 0.2.*
, fclabels == 1.1.*
, uniplate == 1.6.*
, syb == 0.3.* && >= 0.3.3
, binary == 0.5.*
, derive == 2.5.*
, time >= 1.2 && < 1.5
, parallel == 3.2.*
, HUnit == 1.2.*
, tamarin-prover-utils == 0.4.*
, tamarin-prover-term == 0.4.*
other-modules:
Paths_tamarin_prover
Main_NoGui
Main_Full
Main.Console
Main.Environment
Main.TheoryLoader
Main.Utils
Main.Mode.Test
Main.Mode.Batch
Main.Mode.Intruder
Main.Mode.Interactive
Theory.AbstractInterpretation
Theory.Pretty
Theory.Fact
Theory.Atom
Theory.Formula
Theory.Rule
Theory.IntruderRules
Theory.Proof.Guarded
Theory.Proof.Types
Theory.Proof.EquationStore
Theory.Proof.SolveGuarded
Theory.Proof.Sequent
Theory.Proof.Sequent.Dot
Theory.Proof.CaseDistinctions
Theory.Proof
Theory.RuleVariants
Theory.RuleSet
Theory.Signature
Theory
Theory.Lexer
Theory.Parser
Theory.Wellformedness
Web.Settings
Web.Types
Web.Theory
Web.Hamlet
Web.Instances
Web.Handler
Web.Dispatch