@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@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}
}