Visible to the public A Symbolic Analysis of ECC-Based Direct Anonymous Attestation

TitleA Symbolic Analysis of ECC-Based Direct Anonymous Attestation
Publication TypeConference Paper
Year of Publication2019
AuthorsWhitefield, J., Chen, L., Sasse, R., Schneider, S., Treharne, H., Wesemeyer, S.
Conference Name2019 IEEE European Symposium on Security and Privacy (EuroS P)
KeywordsAnalytical models, authentication, composability, cryptographic protocols, cryptographic scheme, cyber-physical system security, digital signatures, direct anonymous attestation, ECC-based direct anonymous attestation, ECC-based version, ECC-DAA, expected authentication, formal analysis, formal verification, IEC standards, ISO standards, mechanised analysis, neural style transfer, Predictive Metrics, privacy, pubcrawl, public key cryptography, Resiliency, Scalability, secrecy, secrecy properties, symbol manipulation, symbolic analysis, symbolic verification, Tamarin modelling, Tamarin prover, TPM, Trusted Computing, trusted platform module TPM-backed anonymous credentials, trusted platform modules
AbstractDirect Anonymous Attestation (DAA) is a cryptographic 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.
Citation Keywhitefield_symbolic_2019