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.