Verification of Stateful Cryptographic Protocols with Exclusive OR
| Autor: | Jannik Dreier, Saša Radomirović, Lucca Hirschi, Ralf Sasse |
|---|---|
| Přispěvatelé: | Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), School of Computing [Dundee], University of Dundee, Institute of Information Security [ETH Zürich], Department of Computer Science [ETH Zürich] (D-INFK), Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich)- Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Theoretical computer science
Computer Networks and Communications Computer science Exclusive or 02 engineering and technology Gas meter prover Mathematical proof [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR] Stateful firewall 0202 electrical engineering electronic engineering information engineering Computer Science::Networking and Internet Architecture 0501 psychology and cognitive sciences Observational equivalence Safety Risk Reliability and Quality formal verification Formal verification Computer Science::Cryptography and Security 05 social sciences 020206 networking & telecommunications Cryptographic protocol Hardware and Architecture State (computer science) exclusive or Software 050104 developmental & child psychology cryptographic protocols |
| Zdroj: | Journal of Computer Security Journal of Computer Security, IOS Press, 2020, 28 (1), pp.1--34. ⟨10.3233/JCS-191358⟩ Journal of Computer Security, 2020, 28 (1), pp.1--34. ⟨10.3233/JCS-191358⟩ |
| ISSN: | 0926-227X 1875-8924 |
| DOI: | 10.3233/JCS-191358⟩ |
| Popis: | International audience; In cryptographic protocols, in particular RFID protocols, exclusive-or (XOR) operations are common. Due to the inherent complexity of faithful models of XOR, there is only limited tool support for the verification of cryptographic protocols using XOR. In this paper, we improve the TAMARIN prover and its underlying theory to deal with an equational theory modeling XOR operations. The XOR theory can be combined with all equational theories previously supported, including user-defined equational theories. This makes TAMARIN the first verification tool for cryptographic protocols in the symbolic model 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|