Formal Verification of Security and Privacy Requirements in Modern ICT Systems Assisted by the Tamarin Security-protocol Prover
ABSTRACT
Over the last 3-5 years, we developed several formal-methods theories in order to be able to verify specific aspects of security and privacy in different modern and protocols. These theories were then implemented entirely or via some approximation in formal specifications in the Tamarin prover [6]. In turn, these models allowed us to assess in practical mechanisation of theorem proving a range of security and privacy requirements in a number of modern and complex systems: from paymentsecurity in in plastic-cards and mobile-applications’ EMV (Europay Mastercard Visa) electronic payments [3], as well as their contactless/proximity robustness [4], to authentication in IoT protocols [5] or furthermore their privacy properties [1], and classical as well as post-compromise keyexchange security in mobile procedures [2]. Not only that, but –in this way— we uncovered a series of vulnerabilities in these systems and proposed a number of patches, which we then proved secure/private/correct via the same Tamarin-assisted methodology.
Furthermore, these lines of work influenced the EMV standard (i.e., [4]) and the 3GPP standard (i.e., [2]), lead to an on-going amendment of the ISO 14443 standard (i.e., [3]) and the LoRaWAN specification version 1.1 (i.e., [5]) and its upcoming version 1.2 (i.e., [1]), as well as made front-page news on all media outlets1 (i.e., [3]).
In this talk, we will develop on several of the theoretical underpinnings that got incorporated into the Tamarin models that lead to these impacts. Also, we will look at certain practical intricacies of the Tamarin models themselves, including aspects that generally lead to intractability, as well as Tamarin-“oracles” writing. Finally, we will discuss some of the disclosure process and standardisation work that ensued.
Author
Ioana is a Professor in Secure Systems at the University of Surrey. She is also the Deputy Director of the Surrey Centre for Cyber Security (SCCS), and Co-Director of Surrey's Gold-level ACE-CSE Academic Centre of Excellence in Cyber Security Education. From October 2021 to June 2022, she was a Royal-Society Leverhulme Senior Research Fellow. Her research interests are in area of cyber security, formal verification and cryptography, with a focus on, (a) formal security analysis -- development of formal frameworks and tools for protocol analysis, (b) provable security -- generic framework development, protocol design, security proofs.
References
[1] K. Budykho, I. Boureanu, S. Wesemeyer, F. Rajaona, D. Romero, M. Lewis, Y. Rahulan, S. Schneider, "Fine- Grained Trackability in Protocol Executions", Network and Distributed System Security Symposium (NDSS) 2023, 2023
[2] R. Miller, I. Boureanu, S. Wesemeyer, C. Newton, "The 5G Key-Establishment Stack: In-Depth Formal Verification and Experimentation", at the 17th ACM ASIA Conference on Computer and Communications Security (ACM ASIACCS), 2022
[3] A. Radu, T. Chothia, C. Newton, I. Boureanu, L. Chen, "Practical EMV Relay Protection", at the 2022 IEEE Symposium on Security and Privacy (IEEE S & P, 2022)
[4] I. Boureanu, T. Chothia, A. Debant, S. Delaune, "Security Analysis and Implementation of Relay-Resistant Contactless Payments", at the 27th ACM Conference on Computer and Communications Security (ACM CCS 2020)
[5] S. Wesemeyer, I. Boureanu, Z. Smith, H. Treharne, "Extensive Security Verification of LoRaWAN Key Establishment: Insecurities and Patches", at the 5th IEEE European Symposium on Security and Privacy (IEEE Euro S & P 2020) [6] S. Meier, B. Schmidt, C. Cremers, and D. Basin. The TAMARIN prover for the symbolic analysis of security protocols. In CAV ’13, LNCS, pages 696–701. Springer. ISBN 978-3-642- 39799-8