Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR

Jannik Dreier, Lucca Hirschi, Saša Radomirović, Ralf Sasse

Research output: Chapter in Book/Report/Conference proceedingConference contribution

37 Citations (Scopus)
270 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publication2018 IEEE 31st Computer Security Foundations Symposium (CSF)
PublisherIEEE
ChapterSession: Security Protocols 2
Pages359-373
Number of pages15
Edition31st
ISBN (Print)9781538666807
DOIs
Publication statusPublished - 7 Aug 2018
Event31st IEEE Computer Security Foundations Symposium - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018
Conference number: 31
https://www.cs.ox.ac.uk/conferences/csf2018/index.html

Conference

Conference31st IEEE Computer Security Foundations Symposium
Abbreviated titleCSF2018
Country/TerritoryUnited Kingdom
CityOxford
Period9/07/1812/07/18
Internet address

Keywords

  • Cryptographic-Protocols
  • Exclusive-OR
  • Formal-Verification
  • Symbolic-Model
  • Tamarin

ASJC Scopus subject areas

  • General Engineering

Fingerprint

Dive into the research topics of 'Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR'. Together they form a unique fingerprint.

Cite this