Tamarin Prover

The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification of security protocols specified as multiset rewriting systems with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation combined with a user-defined subterm-convergent rewriting theory.

Authors: Simon Meier, Benedikt Schmidt — Contributors: Cas Cremers, Cedric Staub — Observational Equivalence authors: Jannik Dreier, Ralf Sasse

Research papers and theses on Tamarin




The Tamarin prover is open-source software. Its code and issue tracker are available at https://github.com/tamarin-prover/tamarin-prover. Its low-volume mailing list for announcements and discussion is https://groups.google.com/group/tamarin-prover.



Installation instructions are in the INSTALLATION.md in the Github repository.



Page URL: http://www.infsec.ethz.ch/research/software/tamarin.html
© 2015 Eidgenössische Technische Hochschule Zürich