The tamarin-prover package

[Tags: gpl, program]

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 (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 here: http://www.infsec.ethz.ch/research/software#TAMARIN


Properties

Versions0.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
Dependenciesaeson (==0.3.*), array (==0.3.*), base (==4.*), binary (==0.5.*), blaze-builder (==0.3.*), bytestring (==0.9.*), cmdargs (>=0.6.8 && <0.7), containers (>=0.3 && <0.4.2), deepseq (==1.1.*), derive (==2.5.*), directory (>=1.0 && <1.2), fclabels (==1.0.*), filepath (>=1.1 && <1.3), hamlet (==0.8.*), http-types (==0.6.*), monad-control (==0.2.*), mtl (==2.0.*), old-locale (==1.0.*), parallel (==3.2.*), parsec (==3.1.*), process (==1.0.*), safe (>=0.2 && <0.4), syb (>=0.3.3 && <0.4), tamarin-prover-term (==0.1.*), tamarin-prover-utils (==0.1.*), text (==0.11.*), threads (==0.4.*), time (==1.2.*), transformers (==0.2.*), uniplate (==1.6.*), wai (==0.4.*), warp (==0.4.*), yesod-core (==0.8.*), yesod-form (==0.1.*), yesod-json (==0.1.*), yesod-static (==0.1.*)
LicenseGPL
CopyrightBenedikt Schmidt, Simon Meier, ETH Zurich, 2010-2012
AuthorBenedikt Schmidt <benedikt.schmidt@inf.ethz.ch>, Simon Meier <simon.meier@inf.ethz.ch>
MaintainerSimon Meier <simon.meier@inf.ethz.ch>
CategoryTheorem Provers
Home pagehttp://www.infsec.ethz.ch/research/software#TAMARIN
Executablestamarin-prover
Upload dateFri Feb 10 21:30:09 UTC 2012
Uploaded bySimonMeier
Downloads575 total (66 in last 30 days)

Flags

NameDescriptionDefault
threadedBuild with support for multithreaded executionEnabled
test-coverageBuild with test coverage supportEnabled
build-testsBuild unit test driverDisabled

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

Downloads

Maintainers' corner

For package maintainers and hackage trustees