| Title | A Symbolic Analysis of ECC-Based Direct Anonymous Attestation |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Whitefield, J., Chen, L., Sasse, R., Schneider, S., Treharne, H., Wesemeyer, S. |
| Conference Name | 2019 IEEE European Symposium on Security and Privacy (EuroS P) |
| Keywords | Analytical 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 |
| Abstract | Direct 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. |
| DOI | 10.1109/EuroSP.2019.00019 |
| Citation Key | whitefield_symbolic_2019 |
A Symbolic Analysis of ECC-Based Direct Anonymous Attestation