cabal-version: >= 1.8 build-type: Simple name: tamarin-prover version: 0.1.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 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 () as a unification backend and GraphViz () to visualize constraint systems. Detailed instructions for installing the `tamarin` prover are given here: 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