Abstract
A definition of user-controlled anonymity is introduced for Direct Anonymous Attestation schemes. The definition is expressed as an equivalence property suited to automated reasoning using ProVerif and the practicality of the definition is demonstrated by examining the ECCbased Direct Anonymous Attestation protocol by Brickell, Chen & Li.We show that this scheme satisfies our definition under the assumption that the adversary obtains no advantage from re-blinding a blind signature.