BEGIN:VCALENDAR VERSION:2.0 PRODID:-//wp-events-plugin.com//7.2.3.1//EN BEGIN:VEVENT UID:794@lincs.fr DTSTART;TZID=Europe/Paris:20231220T103000 DTEND;TZID=Europe/Paris:20231220T113000 DTSTAMP:20240122T123339Z URL:https://www.lincs.fr/events/proving-and-analysing-security-protocols-w ith-tamarin-prover/ SUMMARY:Proving and analysing security protocols with Tamarin Prover DESCRIPTION: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].\n\nIn 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.\n\nThe presentation is an adapted material from the Tamarin Prover's manual and is available under the CC BY-NC-SA 4.0 license.\n\nSlides\n\nPrerequisites for the participants who want to use the tool:\n- Windows: install Windows Subsystem for Linux (WSL) - https://learn.microsoft.com/en-gb/windows/wsl/install\, then install Homebrew - https://brew.sh/\n- macOS &\; Linux: install Homebrew - https://brew.sh/\n\nWebsite: https://tamarin-prover.com/\nUser manual: https://tamarin-prover.com/manual/\nTeaching materials: https://github.com/tamarin-prover/teaching\nGoogle Groups: https://groups.google.com/g/tamarin-prover\nSource code: https://github.com/tamarin-prover/tamarin-prover\nLicense: GNU GPL v3\n\nResearch materials: https://tamarin-prover.com/#research_papers_and_theses\n\n---\nReferences:\ n\n[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\n\n[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/informat ion-security-group-dam/research/software/TLS-1.3_thesis_vincent_stettler.pd f\n\n[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\n\n[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/informat ion-security-group-dam/research/software/5G_lanzenberger.pdf\n\n[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\n\n[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\n\n[ 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\n\n [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 CATEGORIES:Network Theory,Working Group,Youtube LOCATION:Room 4A113\, 19 place Marguerite Perey\, Palaiseau\, France X-APPLE-STRUCTURED-LOCATION;VALUE=URI;X-ADDRESS=19 place Marguerite Perey\, Palaiseau\, France;X-APPLE-RADIUS=100;X-TITLE=Room 4A113:geo:0,0 END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:STANDARD DTSTART:20231029T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET END:STANDARD END:VTIMEZONE END:VCALENDAR