Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes

Ben Smyth, Mark D. Ryan & Liqun Chen (2011) Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes. In FAST'11: 8th International Workshop on Formal Aspects of Security and Trust, LNCS 7140, Springer, pp. 245-262.

See Cryptology ePrint Archive version.

Download

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 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.

Bibtex Entry

@inproceedings{2011-anonymity-definition-for-Direct-Anonymous-Attestation,
	author = "Ben Smyth and Mark D. Ryan and Liqun Chen",
	title = "{Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes}",
	year = "2011",
	booktitle = "FAST'11: 8th International Workshop on Formal Aspects of Security and Trust",
	publisher = "Springer",
	series = "LNCS",
	volume = "7140",
	pages = "245--262",
	doi = "10.1007/978-3-642-29420-4_16",
}