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.