Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme

Direct Anonymous Attestation (Daa) is a set of cryptographic schemes used to create anonymous digital signatures. To provide additional assurance, Daa schemes can utilise a Trusted Platform Module (Tpm) that is a tamper-resistant hardware device embedded in a computing platform and which provides cryptographic primitives and secure storage. We extend Chen and Li's Daa scheme to support: 1) signing a message anonymously, 2) self-certifying Tpm keys, and 3) ascertaining a platform's state as recorded by the Tpm's platform configuration registers (PCR) for remote attestation, with explicit reference to Tpm2.0 API calls. We perform a formal analysis of the scheme and are the first symbolic models to explicitly include the low-level Tpm call details. Our analysis reveals that a fix pro-posed by Whitefield et al. to address an authentication attack on an Ecc-Daa scheme is also required by our scheme. Developing a fine-grained, formal model of a Daa scheme contributes to the growing body of work demonstrating the use of formal tools in supporting security analyses of cryptographic protocols. We additionally provide and benchmark an open-source C++implementation of this Daa scheme supporting both a hardware and a software Tpm and measure its performance.