Many cryptographic security definitions can be naturally
formulated as observational equivalence properties. However,
existing automated tools for verifying the observational
equivalence of cryptographic protocols are limited: they do not
handle protocols with mutable state and an unbounded number of
sessions. We propose a novel definition of observational
equivalence for multiset rewriting systems. We then extend the
Tamarin prover, based on multiset rewriting, to prove the
observational equivalence of protocols with mutable state, an
unbounded number of sessions, and equational theories such as
Diffie-Hellman exponentiation. We demonstrate its effectiveness
on case studies, including a stateful TPM protocol.