Direct Anonymous Attestation (DAA) is a crypto-
graphic scheme that provides Trusted Platform Module (TPM)-
backed anonymous credentials. We develop TAMARIN modelling
of the ECC-based version of the protocol as it is standardised
and provide the first mechanised analysis of this standard. Our
analysis confirms that the scheme is secure when all TPMs are
assumed honest, but reveals a break in the protocol’s expected
authentication and secrecy properties for all TPMs even if only
one is compromised. We propose and formally verify a minimal
fix to the standard. In addition to developing the first formal
analysis of ECC-DAA , the paper contributes to the growing body
of work demonstrating the use of formal tools in supporting
standardisation processes for cryptographic protocols.