Abstract
The privacy-CA solution (PCAS) designed by the Trusted Computing Group (TCG) was specified in TCG Trusted Platform Module (TPM) Specification Version 1.2 in 2003 and allows a TPM to obtain from a certification authority (CA) certificates on short term keys. The PCAS protocol is a lighter alternative to the Direct Anonymous Attestation (DAA) scheme for anonymous platform authentication.
The first rigorous analysis of PCAS was recently performed by Chen and Warinschi who focus on an unforgeability property (a TPM cannot obtain a certificate without the CA knowing its identity). The analysis in that paper holds only when no TPM is corrupt as, otherwise, an attack can be easily mounted. The authors also propose a stronger protocol (which we refer to as the enhanced PCAS or ePCAS) intended to withstand attacks of corrupt TPMs, but the protocol had never been formally analyzed.
The contribution of this paper is two-fold. We formalize three security properties desired from the ePCAS protocol. Unforgeability refines the earlier model for the case where TPMs may be corrupted. Deniability is the property that a CA cannot prove to a third party that he engaged in a run of the protocol with a certain TPM. Finally, anonymity is the property that third parties cannot tell the identity of TPMs based on the certificates that the TPM uses. The second contribution are proofs that the ePCAS protocol does indeed satisfy the security requirements that we formalize in this paper.