tamarin-prover-0.1.1.0: tamarin-prover.cabal
cabal-version: >= 1.8
build-type: Simple
name: tamarin-prover
version: 0.1.1.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 is
currently under submission to CSF 2012. Drop us (simon.meier\@inf.ethz.ch
or benedikt.schmidt\@inf.ethz.ch) a mail, if you would like to obtain a
copy of the paper.
.
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 here:
<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
-- 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
-- example files
examples/UserGuide.spthy
examples/TLS.spthy
-- examples/Typing_Invariant_Example.spthy
-- CSF'12 case studies
examples/csf12/Artificial.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_wPFS.spthy
examples/csf12/JKL_TS1_2008-KI.spthy
examples/csf12/JKL_TS2_2004-KI_wPFS.spthy
examples/csf12/JKL_TS2_2004-KI.spthy
examples/csf12/JKL_TS2_2008-KI_wPFS.spthy
examples/csf12/JKL_TS2_2008-KI.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
README
CHANGES
--------------
-- build flags
--------------
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
build-depends:
base == 4.*
, array == 0.3.*
, deepseq == 1.1.*
, containers >= 0.3 && < 0.4.2
, mtl == 2.0.*
, cmdargs == 0.6.* && >= 0.6.8
, filepath >= 1.1 && < 1.3
, directory >= 1.0 && < 1.2
, process == 1.0.*
, parsec == 3.1.*
, bytestring == 0.9.*
, safe >= 0.2 && < 0.4
, transformers == 0.2.*
, fclabels == 1.0.*
, uniplate == 1.6.*
, syb == 0.3.* && >= 0.3.3
, binary == 0.5.*
, derive == 2.5.*
, time == 1.2.*
, threads == 0.4.*
, http-types == 0.6.*
, blaze-builder == 0.3.*
, yesod-core == 0.8.*
, yesod-json == 0.1.*
, yesod-static == 0.1.*
, yesod-form == 0.1.*
, text == 0.11.*
, wai == 0.4.*
, hamlet == 0.8.*
, warp == 0.4.*
, aeson == 0.3.*
, old-locale == 1.0.*
, monad-control == 0.2.*
, parallel == 3.2.*
, tamarin-prover-utils == 0.1.*
, tamarin-prover-term == 0.1.*
-- extra deps to get it building on GHC 7.0.3 without the new modular
--solver of cabal-install, activated with flag --solver=modular
if impl(ghc <= 7.2)
build-depends:
template-haskell == 2.5.*
, data-default == 0.2.*
, wai-extra == 0.4.3
if flag(threaded)
ghc-options: -threaded
ghc-options: -Wall -funbox-strict-fields -fwarn-tabs -rtsopts
main-is: Main.hs
hs-source-dirs: src
other-modules:
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.Signature
Theory
Theory.Lexer
Theory.Parser
Theory.Wellformedness
Web.Settings
Web.Types
Web.Theory
Web.Hamlet
Web.Instances
Web.Handler
Web.Dispatch