Formal analysis of privacy in Direct Anonymous Attestation schemes

Ben Smyth; Mark D. Ryan; Liqun Chen

doi:10.1016/j.scico.2015.04.004

Formal analysis of privacy in Direct Anonymous Attestation schemes

Ben Smyth, Mark D. Ryan, Liqun Chen

Computer Science

Research output: Contribution to journal › Article › peer-review

10 Citations (Scopus)

183 Downloads (Pure)

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 issuers and verifiers. A security fix is identified and the revised protocol is shown to satisfy our definition of privacy.

Original language	English
Pages (from-to)	300-317
Journal	Science of Computer Programming
Volume	111
Issue number	2
Early online date	27 Apr 2015
DOIs	https://doi.org/10.1016/j.scico.2015.04.004
Publication status	Published - 1 Nov 2015

Keywords

Accountability
Applied pi calculus
Direct Anonymous Attestation
Privacy
Trusted computing

Access to Document

10.1016/j.scico.2015.04.004

Smyth_Ryan_Chen_Formal_analysis_privacy_Science_Computer_Programming_2015
NOTICE: this is the author’s version of a work that was accepted for publication. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published as B. Smyth et al., Formal analysis of privacy in Direct Anonymous Attestation schemes, Sci. Comput. Program. (2015), http://dx.doi.org/10.1016/j.scico.2015.04.004
Accepted author manuscript, 407 KBLicence: Other (please specify with Rights Statement)

http://linkinghub.elsevier.com/retrieve/pii/S0167642315000702

Leadership Fellowships 2009 : Analysing Security and Privacy Properties
Ryan, M.
Engineering & Physical Science Research Council
1/04/10 → 30/09/15
Project: Research Councils
Verifying Interoperability requirements in Pervasive Systems
Ryan, M. & Ritter, E.
Engineering & Physical Science Research Council
8/10/08 → 7/03/13
Project: Research Councils

Cite this

@article{0d5ea7e52edc4f0f91f86661ed05dc89,

title = "Formal analysis of privacy in Direct Anonymous Attestation schemes",

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 issuers and verifiers. A security fix is identified and the revised protocol is shown to satisfy our definition of privacy.",

keywords = "Accountability, Applied pi calculus, Direct Anonymous Attestation, Privacy, Trusted computing",

author = "Ben Smyth and Ryan, {Mark D.} and Liqun Chen",

year = "2015",

month = nov,

day = "1",

doi = "10.1016/j.scico.2015.04.004",

language = "English",

volume = "111",

pages = "300--317",

journal = "Science of Computer Programming",

issn = "0167-6423",

publisher = "Elsevier",

number = "2",

}

TY - JOUR

T1 - Formal analysis of privacy in Direct Anonymous Attestation schemes

AU - Smyth, Ben

AU - Ryan, Mark D.

AU - Chen, Liqun

PY - 2015/11/1

Y1 - 2015/11/1

N2 - 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 issuers and verifiers. A security fix is identified and the revised protocol is shown to satisfy our definition of privacy.

AB - 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 issuers and verifiers. A security fix is identified and the revised protocol is shown to satisfy our definition of privacy.

KW - Accountability

KW - Applied pi calculus

KW - Direct Anonymous Attestation

KW - Privacy

KW - Trusted computing

U2 - 10.1016/j.scico.2015.04.004

DO - 10.1016/j.scico.2015.04.004

M3 - Article

SN - 0167-6423

VL - 111

SP - 300

EP - 317

JO - Science of Computer Programming

JF - Science of Computer Programming

IS - 2

ER -

Formal analysis of privacy in Direct Anonymous Attestation schemes

Abstract

Keywords

Access to Document

Projects

Leadership Fellowships 2009 : Analysing Security and Privacy Properties

Verifying Interoperability requirements in Pervasive Systems

Cite this