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. Colin Boyd, Anish Mathuria, Douglas Stebila. "Protocols for Authentication and Key Establishment", Second Edition Springer, 2019. pg 48 Tamarin has automatic proof features, but can also be self-guided. In Tamarin lemmas that representing security properties are defined.Celi, Sofía, Jonathan Hoyland, Douglas Stebila, and Thom Wiggers. "A tale of two models: Formal verification of KEMTLS via Tamarin." In European Symposium on Research in Computer Security, pp. 63-83. Cham: Springer Nature Switzerland, 2022. 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.P. Remlein, M. Rogacki and U. Stachowiak, "Tamarin software – the tool for protocols verification security," 2020 Baltic URSI Symposium (URSI), Warsaw, Poland, 2020, pp. 118-123, doi: 10.23919/URSI48707.2020.9254078.
See also Dolev–Yao model Hybrid argument ProVerif
References
External links Tamarin Prover official website David Wong created an introductory video on the Tamarin Prover.