Paper 2012/650

Formal analysis of privacy in Direct Anonymous Attestation schemes

Ben Smyth, 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.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. This article is a based upon our ESAS'07 & FAST'11 conference papers and Chapter 4 of Smyth's PhD thesis.
Keywords
Accountabilityanonymityapplied pi calculusDirect Anonymous AttestationprivacyProVeriftrusted computingTPMtraceabilityunlinkability.
Contact author(s)
inria @ bensmyth com
History
2015-03-04: last of 2 revisions
2012-11-21: received
See all versions
Short URL
https://ia.cr/2012/650
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2012/650,
      author = {Ben Smyth and Mark D.  Ryan and Liqun Chen},
      title = {Formal analysis of privacy in Direct Anonymous Attestation schemes},
      howpublished = {Cryptology {ePrint} Archive, Paper 2012/650},
      year = {2012},
      url = {https://eprint.iacr.org/2012/650}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.