Anonymous Direct 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 primi- tives 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 TPM 2.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 pro- vide and benchmark an open-source C++ implementation of this DAA scheme supporting both a hardware and a software TPM and measure its performance.