key: 2012-Direct-Anonymous-Attestation-privacy-definition
type: article
title: Formal analysis of privacy in Direct Anonymous Attestation schemes
authors:
  - Ben Smyth
  - Mark D. Ryan
  - Liqun Chen
year: 2015
month: 4
journal: Science of Computer Programming
volume: "111"
number: "2"
doi: 10.1016/j.scico.2015.04.004
description: >-
  This article presents a symbolic definition of user-controlled anonymity for Direct Anonymous
  Attestation schemes suited to automated reasoning using ProVerif.
keywords: >-
  Direct Anonymous Attestation, DAA, trusted computing, Trusted Platform Module, TPM,
  user-controlled anonymity, anonymity, unlinkability, privacy, accountability, traceability,
  ProVerif, applied pi calculus, RSA
abstract: >-
  This article introduces a definition of privacy 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 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.
links:
  - file: Smyth12-privacy-definition-DAA.pdf
    text: Journal article
    alt:
      url: https://eprint.iacr.org/2012/650
      text: Cryptology ePrint Archive version
  - file: Smyth12-RSA-DAA-case-study.tar.gz
    text: ProVerif source
  - url: https://doi.org/10.1016/j.scico.2015.04.004
    text: Official version