Tamarin Prover Explained

Tamarin Prover
Tamarin Prover
Author:David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt
Developer:Cas Cremers, Jannik Dreier, Ralf Sasse
Latest Release Version:1.4.1
Programming Language:Haskell
Operating System:Linux, macOS
Language:English
Genre:Automated reasoning
License:GNU GPL v3

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] 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.[8] Tamarin has automatic proof features, but can also be self-guided. In Tamarin lemmas that representing security properties are defined.[9] 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.[10]

See also

External links

Notes and References

  1. Blanchet, B. (2014). Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif. In: Aldini, A., Lopez, J., Martinelli, F. (eds) Foundations of Security Analysis and Design VII. FOSAD FOSAD 2013 2012. Lecture Notes in Computer Science, vol 8604. Springer, Cham.
  2. Cremers . Cas . Horvat . Marko . Scott . Sam . van der Merwe . Thyla . 2016 . Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication . IEEE Symposium on Security and Privacy, 2016, San Jose, CA, USA, May 22-26, 2016 . 470–485 . IEEE S&P 2016 . 978-1-5090-0824-7 . 10.1109/SP.2016.35.
  3. Basin . David . Cremers . Cas . Meier . Simon . 2013 . Provably repairing the ISO/IEC 9798 standard for entity authentication . Journal of Computer Security . 21 . 6 . 817–846 . 10.3233/JCS-130472. 20.500.11850/69793 .
  4. Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5 . Cremers . Cas . Cas Cremers . Dehnel-Wild . Martin . Milner . Kevin . 2017 . Springer . Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I . 389–407 . 978-3-319-66401-9 . Oslo, Norway . ESORICS 2017 . https://www.ntnu.edu/esorics2017 . 10.1007/978-3-319-66402-6_23.
  5. Automated analysis of Diffie-Hellman protocols and advanced security properties . Schmidt . Benedikt . Meier . Simon . Cremers . Cas . Cas Cremers . Basin . David . 2012 . IEEE Computer Society . 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012 . 78–94 . Cambridge, MA . CSF 2012.
  6. Schmidt . Benedikt . 2012 . Formal analysis of key exchange protocols and physical protocols . ETH Zurich . PhD thesis . 10.3929/ethz-a-009898924 . 20.500.11850/72713 .
  7. Meier . Simon . 2012 . Advancing automated security protocol verification . ETH Zurich . PhD thesis. 10.3929/ethz-a-009790675 . 20.500.11850/66840 .
  8. Colin Boyd, Anish Mathuria, Douglas Stebila. "Protocols for Authentication and Key Establishment", Second Edition Springer, 2019. pg 48
  9. 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.
  10. 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.

This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Tamarin Prover".

Except where otherwise indicated, Everything.Explained.Today is © Copyright 2009-2025, A B Cryer, All Rights Reserved. Cookie policy.