BEAR Applications

Tamarin_prover

The Tamarin prover is a security protocol verification tool that supports both falsification and unbounded verification in the symbolic model. Security protocols are specified as multiset rewriting systems and analysed with respect to (temporal) first-order properties and a message theory that models Diffie-Hellman exponentiation and exclusive-or (XOR), combined with a user-defined rewriting theory that has the Finite Variant Property, which includes subterm-convergent theories.

More Information

For more information visit the Tamarin_prover website.

Available Versions

These versions of Tamarin_prover are available on the BEAR systems (BlueBEAR, BEARCloud VMs, and CaStLeS VMs). These will be retained in accordance with our Applications Support and Retention Policy.