Tamarin Prover
Software for formal verification of cryptographic protocols
From Wikipedia, the free encyclopedia
Tamarin Prover is a computer software program for formal verification of cryptographic protocols.[1] It has been used to verify Transport Layer Security 1.3,[2] ISO/IEC 9798,[3] DNP3 Secure Authentication v5,[4] WireGuard,[5][6][7][8] and the PQ3 Messaging Protocol of Apple iMessage.[9]
| Tamarin Prover | |
|---|---|
| |
 | |
| Original authors | David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt |
| Developers | Cas Cremers, Jannik Dreier, Ralf Sasse |
| Initial release | April 24, 2012 |
| Stable release | 1.4.1
/ January 18, 2019 |
| Written in | Haskell |
| Operating system | Linux, macOS |
| Available in | English |
| Type | Automated reasoning |
| License | GNU GPL v3 |
| Website | tamarin-prover |
| Repository | github |
Tamarin is an open source tool, written in Haskell,[10] built as a successor to an older verification tool called Scyther.[11] Tamarin has automatic proof features, but can also be self-guided.[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.[12][10]