Decidability of Trace Equivalence for Protocols with Nonces

Abstract

Privacy properties such as anonymity, unlink ability, or vote secrecy are typically expressed as equivalence properties. In this paper, we provide the first decidability result for trace equivalence of security protocols, for an unbounded number of sessions and unlimited fresh nonce's. Our class encompasses most symmetric key protocols of the literature, in their tagged variant.