tamarin-prover: The Tamarin prover for security protocol analysis.
Note that the tamarin-prover should be installed from source as
described in its README at
https://github.com/tamarin-prover/tamarin-prover.
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
| Name | Description | Default |
|---|---|---|
| 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
- tamarin-prover-0.8.6.3.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)
Maintainer's Corner
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 2015-09-07T11:51:42Z |
| Distributions | Arch:1.8.0 |
| Reverse Dependencies | 1 direct, 0 indirect [details] |
| Executables | tamarin-prover |
| Downloads | 11529 total (53 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-01 [all 6 reports] |