Biblio

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.

Vehicular communication systems increase traffic efficiency and safety by allowing vehicles to share safety-related information and location-based services. Pseudonym schemes are the standard solutions providing driver/vehicle anonymity, whilst enforcing vehicle accountability in case of liability issues. State-of-the-art PKI-based pseudonym schemes present scalability issues, notably due to the centralized architecture of certificate-based solutions. The first Direct Anonymous Attestation (DAA)-based pseudonym scheme was introduced at VNC 2017, providing a decentralized approach to the pseudonym generation and update phases. The DAA-based construction leverages the properties of trusted computing, allowing vehicles to autonomously generate their own pseudonyms by using a (resource constrained) Trusted Hardware Module or Component (TC). This proposition however requires the TC to delegate part of the (heavy) pseudonym generation computations to the (more powerful) vehicle's On-Board Unit (OBU), introducing security and privacy issues in case the OBU becomes compromised. In this paper, we introduce a novel pseudonym scheme based on a variant of DAA, namely a pre-DAA-based pseudonym scheme. All secure computations in the pre-DAA pseudonym lifecycle are executed by the secure element, thus creating a secure enclave for pseudonym generation, update, and revocation. We instantiate vehicle-to-everything (V2X) with our pre-DAA solution, thus ensuring user anonymity and user-controlled traceability within the vehicular network. In addition, the pre-DAA-based construction transfers accountability from the vehicle to the user, thus complying with the many-to-many driver/vehicle relation. We demonstrate the efficiency of our solution with a prototype implementation on a standard Javacard (acting as a TC), showing that messages can be anonymously signed and verified in less than 50 ms.

For a computing platform that is compliant with the Trusted Platform Module (TPM) standard, direct anonymous attestation (DAA) is an appropriate cryptographic protocol for realizing an anonymous subscription system. This approach takes advantage of a cryptographic key that is securely embedded in the platform's hardware, and enables privacy-preserving authentication of the platform. In all of the existing DAA schemes, the platform suffers from significant computational and communication costs that increase proportionally to the size of the revocation list. This drawback renders the existing schemes to be impractical when the size of the revocation list grows beyond a relatively modest size. In this paper, we propose a novel scheme called Lightweight Anonymous Subscription with Efficient Revocation (LASER) that addresses this very problem. In LASER, the computational and communication costs of the platform's signature are multiple orders of magnitude lower than the prior art. LASER achieves this significant performance improvement by shifting most of the computational and communication costs from the DAA's online procedure (i.e., signature generation) to its offline procedure (i.e., acquisition of keys/credentials). We have conducted a thorough analysis of LASER's performance related features. We have implemented LASER on a laptop with an on-board TPM. To the best of our knowledge, this is the first implementation of a DAA scheme on an actual TPM cryptoprocessor that is compliant with the most recent TPM specification, viz., TPM 2.0.