| Speaker : | Guillaume Nibert |
| UPMC Sorbonne Université | |
| Date: | 20/12/2023 |
| Time: | 10:30 am - 11:30 am |
| Location: | Room 4A113 |
Abstract
Tamarin Prover is an open source model checker for proving and verifying security protocols in the Dolev-Yao symbolic model, initially developed at the Information Security Institute, ETH Zürich. The verification algorithms implemented in Tamarin enable unbounded verification and falsification of the security properties of a protocol to be analysed. Tamarin supports XOR and Diffie-Hellmann exponentiation and has been used to analyse widely deployed protocols such as TLS 1.3 [1, 2, 3], 5G authentication [4, 5, 6] or the IEEE 802.11 WPA2 protocol [7] and its patched version against the KRACK attack [8].
In this session we will get to grips with the tool, formally model protocols, adversaries, security properties and understand the mathematical logic behind these properties. The structure of the presentation follows that of the Tamarin manual.
The presentation is an adapted material from the Tamarin Prover’s manual and is available under the CC BY-NC-SA 4.0 license.
Prerequisites for the participants who want to use the tool:
– Windows: install Windows Subsystem for Linux (WSL) – https://learn.microsoft.com/en-gb/windows/wsl/install, then install Homebrew – https://brew.sh/
– macOS & Linux: install Homebrew – https://brew.sh/
Website: https://tamarin-prover.com/
User manual: https://tamarin-prover.com/manual/
Teaching materials: https://github.com/tamarin-prover/teaching
Google Groups: https://groups.google.com/g/tamarin-prover
Source code: https://github.com/tamarin-prover/tamarin-prover
License: GNU GPL v3
Research materials: https://tamarin-prover.com/#research_papers_and_theses
—
References:
[1] C. Cremers, M. Horvat, S. Scott and T. van der Merwe, Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication, 2016 IEEE Symposium on Security and Privacy (SP), San Jose, CA, USA, 2016, pp. 470-485, doi: 10.1109/SP.2016.35. Available at: https://ieeexplore.ieee.org/abstract/document/7546518
[2] V. Stettler, Formally Analyzing the TLS 1.3 proposal, Bachelor thesis, ETH Zürich, Switzerland, 2016. Available at: https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/TLS-1.3_thesis_vincent_stettler.pdf
[3] C. Cremers, M. Horvat, J. Hoyland, S. Scott, and T. van der Merwe, A Comprehensive Symbolic Analysis of TLS 1.3, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17. New York, NY, USA, 2017, pp. 1773–1788. doi: 10.1145/3133956.3134063. Available at: https://dl.acm.org/doi/10.1145/3133956.3134063
[4] D. Lanzenberger, Formal Analysis of 5G Protocols, Bachelor thesis, ETH Zürich, Switzerland, 2017. Available at: https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/research/software/5G_lanzenberger.pdf
[5] D. Basin, J. Dreier, L. Hirschi, S. Radomirovic, R. Sasse, and V. Stettler, A Formal Analysis of 5G Authentication, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS ’18. New York, NY, USA, 2018, pp. 1383–1396. doi: 10.1145/3243734.3243846. Available at: https://arxiv.org/pdf/1806.10360
[6] C. Cremers and M. Dehnel-Wild, Component-based formal analysis of 5G-AKA: channel assumptions and session confusion, Network and Distributed System Security Symposium (NDSS), 2019, doi: 10.14722/ndss.2019.23394. Available at: https://ora.ox.ac.uk/objects/uuid:650ef867-79e1-476d-a602-e7e28dc64970
[7] C. Cremers, B. Kiesl, and N. Medinger, A Formal Analysis of IEEE 802.11’s WPA2: Countering the Kracks Caused by Cracking the Counters, 29th USENIX Security Symposium (USENIX Security 20), 2020, pp. 1–17. Available at: https://www.usenix.org/conference/usenixsecurity20/presentation/cremers
[8] M. Vanhoef and F. Piessens, Key Reinstallation Attacks: Forcing Nonce Reuse in WPA2, Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS ’17. New York, NY, USA, Oct. 2017, pp. 1313–1328. doi: 10.1145/3133956.3134027. Available at: https://papers.mathyvanhoef.com/ccs2017.pdf