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 31 Aug 2013
Contact author: inria at bensmyth com
Available format(s): PDF | BibTeX Citation
Version: 20130901:051118 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]