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 , Simon Meier maintainer: Simon Meier 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 . . 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 () as a unification backend and GraphViz () to visualize constraint systems. Detailed instructions for installing the Tamarin prover are given at . 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