Cryptology ePrint Archive: Report 2012/650

Formal analysis of privacy in Direct Anonymous Attestation schemes

Ben Smyth and Mark D. Ryan and Liqun Chen

Abstract: This article introduces a definition of privacy for Direct Anonymous Attestation schemes. The definition is expressed as an equivalence property which is suited to automated reasoning using Blanchet's ProVerif. The practicality of the definition is demonstrated by analysing the RSA-based Direct Anonymous Attestation protocol by Brickell, Camenisch & Chen. The analysis discovers a vulnerability in the RSA-based scheme which can be exploited by a passive adversary and, under weaker assumptions, corrupt administrators. A security fix is identified and the revised protocol is shown to satisfy our definition of privacy.

Category / Keywords: cryptographic protocols / Accountability, anonymity, applied pi calculus, Direct Anonymous Attestation, privacy, ProVerif, trusted computing, TPM, traceability, unlinkability.

Publication Info: This article is a based upon our ESAS'07 & FAST'11 conference papers and Chapter 4 of Smyth's PhD thesis.

Date: received 15 Nov 2012, last revised 4 Mar 2015

Contact author: inria at bensmyth com

Available format(s): PDF | BibTeX Citation

Version: 20150304:093617 (All versions of this report)

Short URL: ia.cr/2012/650

Discussion forum: Show discussion | Start new discussion