Symbolic Verification of Cryptographic Protocols

In this crypto bite, we'll explore on a high level how cryptographic protocols are verified in the symbolic Dolev-Yao model using automated tools like Tamarin and ProVerif. Everything here is heavily motivated and influenced by [Basin18, BCM15], and of course, by the series on Key Exchange Protocols.

(... to be written: in the mean time, please refer to the slides in [Basin18] and the literature below).

Extending Tamarin

(... to be written, but see [XSHMWO18]'s contribution SmartVerif for an example)

Sources

Even though a bit older, the talk Automated Analysis of TLS 1.3 by Thyla van der Merwe at the 1st BIU Security Day, The Current State of TLS, May 2, 2016, is worth watching. Newer, improved slides, are in [CHHSM18].

Literature

  • [Basin18] David Basin: Symbolic Verification of Cryptographic Protocols using Tamarin. Summer School on Verification Technology, Systems & Applications. Nancy, France, August 2018. (slides pdf: part 1, part 2, part 3).
  • [BCM15] David Basin, Cas Cremers, Catherine Meadows: Model Checking Security Protocols. May 19, 2015. In: Clarke E., Henzinger T., Veith H., Bloem R. (eds) Handbook of Model Checking. pp 727-762. (link.springer.com paywalled, full pdf)
  • [BCDS17] David Basin, Cas Cremers, Jannik Dreier, Ralf Sasse: Symbolically Analyzing Security Protocols using TAMARIN. In: ACM SIGLOG News, Volume 4 Issue 4, October 2017, pp 19-30. (dl.acm.org paywalled, full pdf)
  • [DY83] Danny Dolev, Andrew C. Yao: On the Security of Public Key Protocols. In: IEEE Transactions on Information Theory, Vol. IT-29, No. 2, March 1983. (full pdf)
  • [AN96] Martin Abadi, Roger Needham: Prudent Engineering Practice for Cryptographic Protocols. In: IEEE Transactions on Software Engineering, Volume 22, Issue 1, January 1996, pp 6-15. (ieee.org paywalled, full pdf)
  • [AN95a] Ross Anderson, Roger Needham: Robustness Principles for Public Key Protocols. In: Lecture Notes in Computer Science, Advances in Cryptology. CRYPTO '95. LNCS Vol. 963. pp 236-247. Springen. (full pdf via link.springer.com, full pdf)
  • [AN95] Ross Anderson and Roger Needham: Programming Satan's Computer. In: Computer Science Today, Lecture Notes in Computer Science LNCS vol. 1000. pp 426-440. 1995. (link.springer.com paywalled, full pdf, full pdf alt. location)
  • [Lowe97] Gavin Lowe: A Hierarchy of Authentication Protocols. In: Proceedings 10th Computer Security Foundations Workshop.10-12 June 1997. IEEE. (ieee.org paywalled, full pdf)
  • [CJ97] John Clark, Jeremy Jacob: A survey of authentication protocol literature, 1997. (full pdf)
  • [HLS03] James Heather, Gavin Lowe, Steve Schneider: How to Prevent Type Flaw Attacks on Security Protocols. In: Journal of Computer Security, Volume 11, Number 2, 2003. (full postscript)
  • [TLS13Tamarin] Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, Thyla van der Merwe: Automated Analysis of TLS 1.3 - Symbolic analysis using the Tamarin Prover (project homepage)
  • [BBK17] Karthikeyan Bhargavan, Bruno Blanchet, Nadim Kobeissi: Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate. In: 2017 IEEE Symposium on Security and Privacy. (full pdf)
  • [RefTLS] Symbolic Verification with ProVerif. Project Website.
  • [Schmidt12] Benedikt Schmidt: Formal Analysis of Key Exchange Protocols and Physical Protocols. PhD Dissertation, ETH-Zürich. 2012. (full pdf, doi)
  • [Meier13] Simon Meier: Advancing Automated Security Protocol Verification. PhD Dissertation, ETH-Zürich. 2013. (full pdf, doi)
  • [SMCB12] Benedikt Schmidt, Simon Meier, Cas Cremers, David Basin: Automated Analysis of Diffie-Hellman Protocols and Advanced Security Properties (Extended Version 1, April 14th, 2012). Original in: CSF '12 Proceedings of the 2012 IEEE 25th Computer Security Foundations Symposium, June 25 - 27, 2012, pp 78-94. (full pdf via ieee.org, full extended pdf)
  • [MSCB13] Simon Meier, Benedikt Schmidt, Cas Cremers, David Basin: The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Sharygina N., Veith H. (eds) Computer Aided Verification. CAV 2013. Lecture Notes in Computer Science, LNCS vol 8044, pp 696-702. Springer, Berlin, Heidelberg. (full pdf via link.springer.com)
  • [RSGLR00] Peter L. Ryan, Steve A. Schneider, Michael H. Goldsmith, Gawin Lowe, A. W. Roscoe: The Modelling and Analysis of Security Protocols: the CSP Approach. 2000. (full pdf)
  • [CHHSM18] Cas Cremers, Marko Horvat, Jonathan Hoyland, Sam Scott, Thyla van der Merwe: Automated Analysis of TLS 1.3. Crypto Welcomes TLS 1.3, 19 August 2018. (slides pdf)
  • [XSHMWO18] Yan Xiong, Chen Su, Wenchao Huang, Fuyou Miao, Wansen Wang, Hengyi Ouyang: Verifying Security Protocols using Dynamic Strategies. 13 December 2018 (full pdf via arxiv.org, SmartVerif github)
  • [CgCDGS16] Katriel Cohn-Gordon, Cas Cremers, Benjamin Dowling, Luke Garratt, Douglas Stebila: A Formal Security Analysis of the Signal Messaging Protocol. Extended Version, November 2017. iacr.org 2016/103. (full pdf)