Formal analysis of privacy in Direct Anonymous Attestation schemes

• We formalise Direct Anonymous Attestation (DAA) protocols in the applied pi calculus and present a definition of privacy.
• Our definition is suited to automated reasoning using ProVerif.
• The application of the definition is demonstrated by analysing privacy in the RSA-based DAA protocol.
• Our analysis discovers a vulnerability in the protocol which allows privacy to be violated.
• We fix the RSA-based DAA protocol and show that the revised scheme is secure in the symbolic model.

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.