Lucca Hirschi


Last Name

Hirschi

First Name

Lucca

ORCID

0000-0003-4572-0581

Organisational unit

Filters

2018 - 201952020 - 20214
Reset filters

Search Results

Publications 1 - 9 of 9
  • POR for Security Protocol Equivalences: Beyond Action-Determinism
    Item type: Conference Paper
    Baelde, David; Delaune, Stéphanie; Hirschi, Lucca (2018)
    Lecture Notes in Computer Science ~ Computer Security: 23rd European Symposium on Research in Computer Security, ESORICS 2018, Barcelona, Spain, September 3-7, 2018, Proceedings, Part 1
  • Fixing the Achilles Heel of E-Voting: The Bulletin Board
    Item type: Working Paper
    Hirschi, Lucca; Schmid, Lara; Basin, David (2020)
    Cryptology ePrint Archive
  • Fixing the Achilles Heel of E-Voting: The Bulletin Board
    Item type: Conference Paper
    Hirschi, Lucca; Schmid, Lara; Basin, David (2021)
    2021 IEEE 34th Computer Security Foundations Symposium (CSF)
    The results of electronic elections should be verifiable so that any cheating is detected. To support this, many protocols employ an electronic bulletin board (BB) for publishing data that can be read by participants and used for verifiability checks. We demonstrate that the BB is itself a security-critical component that has often been treated too casually in previous designs and analyses. In particular, we present novel attacks on the e-voting protocols Belenios, Civitas, and Helios that violate some of their central security claims under realistic system assumptions. These attacks were outside the scope of prior security analyses as their verifiability notions assume an idealized BB.
  • Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR
    Item type: Conference Paper
    Dreier, Jannik; Hirschi, Lucca; Radomirović, Saša; et al. (2018)
    IEEE 31th Computer Security Foundations Symposium: CSF 2018: 9-12 July 2018, Oxford, United Kingdom: Proceedings
    Exclusive-or (XOR) operations are common in cryptographic protocols, in particular in RFID protocols and electronic payment protocols. Although there are numerous applications, due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. The TAMARIN prover is a state-of-the-art verification tool for cryptographic protocols in the symbolic model. In this paper, we improve the underlying theory and the tool to deal with an equational theory modeling XOR operations. The XOR theory can be freely combined with all equational theories previously supported, including user-defined equational theories. This makes TAMARIN the first tool to support simultaneously this large set of equational theories, protocols with global mutable state, an unbounded number of sessions, and complex security properties including observational equivalence. We demonstrate the effectiveness of our approach by analyzing several protocols that rely on XOR, in particular multiple RFID-protocols, where we can identify attacks as well as provide proofs.
  • A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols
    Item type: Conference Paper
    Girol, Guillaume; Hirschi, Lucca; Sasse, Ralf; et al. (2020)
    Proceedings of the 29th USENIX Security Symposium
    The Noise specification describes how to systematically construct a large family of Diffie-Hellman based key exchange protocols, including the secure transports used by WhatsApp, Lightning, and WireGuard. As the specification only makes informal security claims, earlier work has explored which formal security properties may be enjoyed by protocols in the Noise framework, yet many important questions remain open. In this work we provide the most comprehensive, systematic analysis of the Noise framework to date. We start from first principles and, using an automated analysis tool, compute the strongest threat model under which a protocol is secure, thus enabling formal comparison between protocols. Our results allow us to objectively and automatically associate each informal security level presented in the Noise specification with a formal security claim. We also provide a fine-grained separation of Noise protocols that were previously described as offering similar security properties, revealing a subclass for which alternative Noise protocols exist that offer strictly better security guarantees. Our analysis also uncovers missing assumptions in the Noise specification and some surprising consequences, e.g., in some situations higher security levels yield strictly worse security.
  • Verification of stateful cryptographic protocols with exclusive OR
    Item type: Journal Article
    Dreier, Jannik; Hirschi, Lucca; Radomirović, Saša; et al. (2020)
    Journal of Computer Security
  • A Formal Analysis of 5G Authentication
    Item type: Conference Paper
    Basin, David; Dreier, Jannik; Hirschi, Lucca; et al. (2018)
    Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security (CCS'18)
    Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.
  • Symbolic Analysis of Identity-Based Protocols
    Item type: Conference Paper
    Basin, David; Hirschi, Lucca; Sasse, Ralf (2019)
    Lecture Notes in Computer Science ~ Foundations of Security, Protocols, and Equational Reasoning. Essays Dedicated to Catherine A. Meadows
  • A formal analysis of 5G authentication
    Item type: Working Paper
    Basin, David; Dreier, Jannik; Hirschi, Lucca; et al. (2018)
    arXiv
    Mobile communication networks connect much of the world's population. The security of users' calls, SMSs, and mobile data depends on the guarantees provided by the Authenticated Key Exchange protocols used. For the next-generation network (5G), the 3GPP group has standardized the 5G AKA protocol for this purpose. We provide the first comprehensive formal model of a protocol from the AKA family: 5G AKA. We also extract precise requirements from the 3GPP standards defining 5G and we identify missing security goals. Using the security protocol verification tool Tamarin, we conduct a full, systematic, security evaluation of the model with respect to the 5G security goals. Our automated analysis identifies the minimal security assumptions required for each security goal and we find that some critical security goals are not met, except under additional assumptions missing from the standard. Finally, we make explicit recommendations with provably secure fixes for the attacks and weaknesses we found.
Publications 1 - 9 of 9