The privacy-CA solution (\pcas) is a protocol designed by the Trusted Computing Group (TCG) as an alternative to the Direct Anonymous Attestation scheme for anonymous authentication of Trusted Platform Module (TPM). The protocol has been specified in TPM Specification Version 1.2. In this paper we offer a rigorous security analysis of the protocol. We first design an appropriate security model that captures the level of security offered by \pcas. The model is justified via the expected uses of the protocol in real applications. We then prove, assuming standard security notions for the underlying primitives that the protocol indeed meets the security notion that we design. Our analysis sheds some light on the design of the protocol. Finally, we propose a strengthened protocol that meets a stronger notion of security where the adversary is allowed to adaptively corrupt TPMs.