Formal analysis of privacy in Direct Anonymous Attestation schemes ?
We formalise Direct Anonymous Attestation (DAA) protocols in the applied pi calculus and present a definition of privacy. Our definition is suited to automated reasoning using ProVerif. The application of the definition is demonstrated by analysing privacy in the RSA-based DAA protocol. Our analysis discovers a vulnerability in the protocol which allows privacy to be violated. We fix the RSA-based DAA protocol and show that the revised scheme is secure in the symbolic model.
privacy direct anonymous attestation applied pi calculus accountability trusted computing