tamarin-prover-0.8.2.0: tamarin-prover.cabal
cabal-version: >= 1.8
build-type: Simple
name: tamarin-prover
version: 0.8.2.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
-- examples files
examples/Tutorial.spthy
-- classic security protocols
examples/classic/TLS_Handshake.spthy
examples/classic/NSLPK3.spthy
examples/classic/NSPK3.spthy
-- loops
examples/loops/Minimal_Crypto_API.spthy
examples/loops/Minimal_KeyRenegotiation.spthy
examples/loops/Minimal_Create_Use_Destroy.spthy
examples/loops/Minimal_Typing_Example.spthy
examples/loops/Minimal_Loop_Example.spthy
examples/loops/Minimal_HashChain.spthy
examples/loops/Typing_and_Destructors.spthy
examples/loops/JCS12_Typing_Example.spthy
examples/loops/TESLA_Scheme1.spthy
examples/loops/TESLA_Scheme2_lossless.spthy
examples/loops/TESLA_Scheme2.spthy
-- related work
examples/related_work/AIF_Moedersheim_CCS10/Keyserver.spthy
examples/related_work/StatVerif_ARR_CSF11/StatVerif_Security_Device.spthy
examples/related_work/StatVerif_ARR_CSF11/StatVerif_GM_Contract_Signing.spthy
examples/related_work/TPM_DKRS_CSF11/Envelope.spthy
examples/related_work/TPM_DKRS_CSF11/TPM_Exclusive_Secrets.spthy
examples/related_work/YubiSecure_KS_STM12/Yubikey.spthy
examples/related_work/YubiSecure_KS_STM12/Yubikey_and_YubiHSM.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
--------------
-- 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 -eventlog
-- 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)
ghc-options: -with-rtsopts=-N
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.5.*
, http-types == 0.7.*
, blaze-builder == 0.3.*
, yesod-core == 1.1.*
, yesod-json == 1.1.*
, yesod-static == 1.1.*
, conduit == 0.5.*
-- , yesod-form == 0.4.* -- required once we reactivate editing
, text == 0.11.*
, wai == 1.3.*
, hamlet == 1.1.*
, warp == 1.3.*
, aeson == 0.6.*
, old-locale == 1.0.*
, monad-control == 0.3.*
, lifted-base == 0.1.*
, threads >= 0.4 && < 0.6
build-depends:
base == 4.*
, bytestring == 0.9.*
, deepseq == 1.3.*
, array >= 0.3 && < 0.5
, containers >= 0.4.2 && < 0.5
, dlist == 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.8.2 && < 0.9
, tamarin-prover-term >= 0.8.2 && < 0.9
, tamarin-prover-theory >= 0.8.2 && < 0.9
other-modules:
Paths_tamarin_prover
Main
Main_Full
Main_NoGui
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
source-repository head
type: git
location: https://github.com/tamarin-prover/tamarin-prover.git