SPOOC: Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR

Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR

Jannik Dreier, Lucca Hirschi, Sasa Radomirovic, and Ralf Sasse. Automated Unbounded Verification of Stateful Cryptographic Protocols with Exclusive OR. In Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF'18), pp. 359–373, IEEE Computer Society Press, Oxford, UK, July 2018.
doi:10.1109/CSF.2018.00033

Download

[PDF] [HTML]

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.

BibTeX

@inproceedings{DHRS-csf18,
  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.},
  address =	 {Oxford, UK},
  author =	 {Dreier, Jannik and Hirschi, Lucca and Radomirovic,
                  Sasa and Sasse, Ralf},
  booktitle =	 {{P}roceedings of the 31st IEEE Computer Security
                  Foundations Symposium (CSF'18)},
  month =	 jul,
  pages =	 359--373,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {Automated Unbounded Verification of Stateful
                  Cryptographic Protocols with Exclusive {OR}},
  year =	 2018,
  acronym =	 {{CSF}'18},
  nmonth =	 7,
                  ={https://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=8429317},
  doi =		 {10.1109/CSF.2018.00033}
}