The privacy-CA solution (PCAS) designed by the Trusted Computing Group (TCG) was specied in TCG Trusted Platform Module (TPM) Specification Version 1.2 in 2003 and allows a TPM to obtain from a certication 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 certicate 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 renes 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 certicates 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.