Smyth, B., Ryan, M., & Chen, L. (2011) Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes. In Proceedings of the eighth International Workshop on Formal Aspects of Security and Trust (FAST'11). Lecture Notes in Computer Science (LNCS), volume 7140, Springer-Verlag, to appear.
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 ECC-based Direct Anonymous Attestation protocol by Brickell, Chen & Li. We show that this scheme is secure under the assumption that the adversary obtains no advantage from re-blinding a blind signature.