Formal analysis of privacy in Direct Anonymous Attestation schemes

Research output: Contribution to journalArticle

Authors

Colleges, School and Institutes

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.

Details

Original languageEnglish
Pages (from-to)300-317
JournalScience of Computer Programming
Volume111
Issue number2
Early online date27 Apr 2015
Publication statusPublished - 1 Nov 2015

Keywords

  • Accountability, Applied pi calculus, Direct Anonymous Attestation, Privacy, Trusted computing