Tamarin Prover
| Tamarin Prover | |
|---|---|
| Original author(s) | David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt |
| Developer(s) | Cas Cremers, Jannik Dreier, Ralf Sasse |
| Initial release | April 24, 2012 |
| Stable release | 1.4.1
/ January 18, 2019 |
| Repository | github |
| Written in | Haskell |
| Operating system | Linux, macOS |
| Available in | English |
| Type | Automated reasoning |
| License | GNU GPL v3 |
| Website | tamarin-prover |
Tamarin Prover is a computer software program for formal verification of cryptographic protocols. It has been used to verify Transport Layer Security 1.3, ISO/IEC 9798, DNP3 Secure Authentication v5, WireGuard, and the PQ3 Messaging Protocol of Apple iMessage.
Tamarin is an open source tool, written in Haskell, built as a successor to an older verification tool called Scyther. Tamarin has automatic proof features, but can also be self-guided. In Tamarin lemmas that representing security properties are defined. After changes are made to a protocol, Tamarin can verify if the security properties are maintained. 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.