The tamarin-prover package

[Tags: deprecated, gpl, program]


Note that the tamarin-prover should be installed from source as described in its README at

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


Change logNone available
Dependenciesaeson (==0.6.*), array (>=0.3), base (==4.*), binary (==0.5.*), blaze-builder (>=0.3), blaze-html (>=0.5), bytestring (>=0.9), cmdargs (==0.10.*), conduit (==1.0.*), containers (>=0.4.2), deepseq (>=1.3), derive (==2.5.*), directory (>=1.0), dlist (>=0.5), fclabels (==1.1.*), filepath (>=1.1), hamlet (>=1.1), http-types (>=0.7), HUnit (==1.2.*), lifted-base (>=, monad-control (==0.*), mtl (>=2.1), old-locale (==1.*), parallel (==3.2.*), parsec (==3.1.*), process (==1.1.*), safe (>=0.2), shakespeare (==2.0.*), syb (>=0.3.3), tamarin-prover-term (>= && <0.9), tamarin-prover-theory (>= && <0.9), tamarin-prover-utils (>= && <0.9), text (==0.11.*), threads (>=0.4), time (>=1.2), transformers (>=0.3), uniplate (==1.6.*), wai (>=1.3), warp (>=1.3), yesod-core (>=, yesod-json (>=1.2), yesod-static (>=1.2) [details]
CopyrightBenedikt Schmidt, Simon Meier, ETH Zurich, 2010-2013
AuthorBenedikt Schmidt <>, Simon Meier <>
MaintainerSimon Meier <>
CategoryTheorem Provers
Home page
Source repositoryhead: git clone
UploadedMon Sep 7 11:51:42 UTC 2015 by SimonMeier
Downloads2257 total (139 in last 30 days)
0 []
StatusDocs not available [build log]
All reported builds failed as of 2015-09-30 [all 2 reports]


no-guiDo not build the web-application GUI.DisabledAutomatic
threadedBuild with support for multithreaded executionEnabledAutomatic
test-coverageBuild with test coverage supportEnabledAutomatic
build-testsBuild unit test driverDisabledAutomatic

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


Maintainers' corner

For package maintainers and hackage trustees