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 , 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 -- 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