Tamarin Prover is a computer software program for formal verification of cryptographic protocols.

[9] Tamarin is an open source tool, written in Haskell,[10] built as a successor to an older verification tool called Scyther.

[11] In Tamarin lemmas that representing security properties are defined.

[12] After changes are made to a protocol, Tamarin can verify if the security properties are maintained.

[12] The results of a Tamarin execution will either be a proof that the security property holds within the protocol, an example protocol run where the security property does not hold, or Tamarin could potentially fail to halt.