tamarin-prover: The Tamarin prover for security protocol analysis.

[ deprecated, program, theorem-provers ] [ Propose Tags ]
Deprecated

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.

Flags

Automatic Flags
NameDescriptionDefault
no-gui

Do not build the web-application GUI.

Disabled
threaded

Build with support for multithreaded execution

Enabled
test-coverage

Build with test coverage support

Enabled
build-tests

Build unit test driver

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1.0.0, 0.1.1.0, 0.4.0.0, 0.4.1.0, 0.6.0.0, 0.6.1.0, 0.8.0.0, 0.8.1.0, 0.8.2.0, 0.8.2.1, 0.8.4.0, 0.8.5.0, 0.8.5.1, 0.8.6.0, 0.8.6.1, 0.8.6.2, 0.8.6.3
Dependencies aeson (>=0.6 && <0.7), array (>=0.3), base (>=4 && <5), binary (>=0.5 && <0.6), blaze-builder (>=0.3), blaze-html (>=0.5), bytestring (>=0.9), cmdargs (>=0.10 && <0.11), conduit (>=1.0 && <1.1), containers (>=0.4.2), deepseq (>=1.3), derive (>=2.5 && <2.6), directory (>=1.0), dlist (>=0.5), fclabels (>=1.1 && <1.2), filepath (>=1.1), hamlet (>=1.1), http-types (>=0.7), HUnit (>=1.2 && <1.3), lifted-base (>=0.2.0.5), monad-control (<1), mtl (>=2.1), old-locale (>=1 && <2), parallel (>=3.2 && <3.3), parsec (>=3.1 && <3.2), process (>=1.1 && <1.2), safe (>=0.2), shakespeare (>=2.0 && <2.1), syb (>=0.3.3), tamarin-prover-term (>=0.8.5.1 && <0.9), tamarin-prover-theory (>=0.8.6.0 && <0.9), tamarin-prover-utils (>=0.8.5.1 && <0.9), text (>=0.11 && <0.12), threads (>=0.4), time (>=1.2), transformers (>=0.3), uniplate (>=1.6 && <1.7), wai (>=1.3), warp (>=1.3), yesod-core (>=1.2.6.6), yesod-json (>=1.2), yesod-static (>=1.2) [details]
License LicenseRef-GPL
Copyright Benedikt Schmidt, Simon Meier, ETH Zurich, 2010-2013
Author Benedikt Schmidt <benedikt.schmidt@inf.ethz.ch>, Simon Meier <simon.meier@inf.ethz.ch>
Maintainer Simon Meier <simon.meier@inf.ethz.ch>
Category Theorem Provers
Home page http://www.infsec.ethz.ch/research/software/tamarin
Source repo head: git clone https://github.com/tamarin-prover/tamarin-prover.git
Uploaded by SimonMeier at 2014-06-08T14:47:32Z
Distributions Arch:1.8.0
Reverse Dependencies 1 direct, 0 indirect [details]
Executables tamarin-prover
Downloads 11296 total (25 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-14 [all 6 reports]