key: 2011-anonymity-definition-for-Direct-Anonymous-Attestation
type: inproceedings
title: Formal analysis of anonymity in ECC-based Direct Anonymous Attestation schemes
authors:
  - Ben Smyth
  - Mark D. Ryan
  - Liqun Chen
year: 2011
month: 9
booktitle: "FAST'11: 8th International Workshop on Formal Aspects of Security and Trust"
series: LNCS
volume: "7140"
pages: 245--262
publisher: Springer
doi: 10.1007/978-3-642-29420-4_16
description: >-
  This paper 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, privacy, ProVerif, applied pi calculus, ECC
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.
supersededby:
  - key: 2012-Direct-Anonymous-Attestation-privacy-definition
    text: Cryptology ePrint Archive version
links:
  - file: Smyth11-definition-anonmity-DAA.pdf
    text: Conference paper
  - file: Smyth11-definition-anonmity-DAA.code.tar.gz
    text: ProVerif source
  - url: https://doi.org/10.1007/978-3-642-29420-4_16
    text: Official version