Authentication of the Command TPM_CertifyKey in the Trusted Platform Module

Donglai FU, Xinguang PENG, Yuli YANG


Trusted Platform Module (TPM) is a key component designed to enable computers achieve greater security. Several vulnerabilities discovered in the TPM highlight the necessity of formal analysis. The procedure invoking an API may be regarded as several interactive processes between the TPM and a user. As a result, the current study formalized the API specifications proposed by Trusted Computing Group (TCG) using applied pi calculus. Meanwhile, two authentication properties between them were also described in a formalized way. With the help of the tool ProVerif, the flaw of the command TPM_CertifyKey was discovered. It was also confirmed on the TPM emulator. Subsequently, the modified API was presented and its authentication properties could be satisfied after verifying again. Results show the model is valid.



Full Text:



  • There are currently no refbacks.

Creative Commons License
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License