Software:Tamarin Prover

From HandWiki
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 releaseScript error: No such module "Date time".
Stable release
1.4.1 / Script error: No such module "Date time".
Repositorygithub.com/tamarin-prover/tamarin-prover
Written inHaskell
Operating systemLinux, macOS
Available inEnglish
TypeAutomated reasoning
LicenseGNU GPL v3
Websitetamarin-prover.github.io

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 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]

See also

References

  1. ↑ Blanchet, Bruno (2014). "Automatic Verification of Security Protocols in the Symbolic Model: The Verifier ProVerif". Foundations of Security Analysis and Design VII. Lecture Notes in Computer Science. 8604. pp. 54–87. doi:10.1007/978-3-319-10082-1_3. ISBN 978-3-319-10081-4. https://doi.org/10.1007/978-3-319-10082-1_3. 
  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 S&P 2016. pp. 470–485. doi:10.1109/SP.2016.35. ISBN 978-1-5090-0824-7. https://tls13tamarin.github.io/TLS13Tamarin/. 
  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. doi:10.3233/JCS-130472. https://www.cs.ox.ac.uk/people/cas.cremers/downloads/papers/BCM2013-iso9798-JCS.pdf. 
  4. ↑ Cremers, Cas; Dehnel-Wild, Martin; Milner, Kevin (2017). "Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5". ESORICS 2017. Oslo, Norway: Springer. pp. 389–407. doi:10.1007/978-3-319-66402-6_23. ISBN 978-3-319-66401-9. http://www.cs.ox.ac.uk/people/cas.cremers/downloads/papers/CrDeMi2017-DNP3-extended.pdf. 
  5. ↑ Donenfeld, Jason A.; Milne, Kevin (2018), Formal Verification of the WireGuard Protocol, https://www.wireguard.com/papers/wireguard-formal-verification.pdf, retrieved 2023-11-23 ; Donenfeld, Jason A., Formal Verification, https://www.wireguard.com/formal-verification/, retrieved 2023-11-23 
  6. ↑ Schmidt, Benedikt; Meier, Simon; Cremers, Cas; Basin, David (2012). "Automated analysis of Diffie-Hellman protocols and advanced security properties". CSF 2012. Cambridge, MA: IEEE Computer Society. pp. 78–94. https://www.cs.ox.ac.uk/people/cas.cremers/downloads/papers/ScMeCrBa2012-tamarin.pdf. 
  7. ↑ Schmidt, Benedikt (2012). Formal analysis of key exchange protocols and physical protocols (PhD thesis). ETH Zurich. doi:10.3929/ethz-a-009898924. hdl:20.500.11850/72713.
  8. ↑ Meier, Simon (2012). Advancing automated security protocol verification (PhD thesis). ETH Zurich. doi:10.3929/ethz-a-009790675. hdl:20.500.11850/66840.
  9. ↑ Basin, David; Linker, Felix; Sasse, Ralf, A Formal Analysis of the iMessage PQ3 Messaging Protocol, https://security.apple.com/assets/files/A_Formal_Analysis_of_the_iMessage_PQ3_Messaging_Protocol_Basin_et_al.pdf, retrieved 2024-03-06 
  10. ↑ 10.0 10.1 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.
  11. ↑ 11.0 11.1 Colin Boyd, Anish Mathuria, Douglas Stebila. "Protocols for Authentication and Key Establishment", Second Edition Springer, 2019. pg 48
  12. ↑ 12.0 12.1 12.2 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.



Retrieved from "https://handwiki.org/wiki/index.php?title=Software:Tamarin_Prover&oldid=3966976"