Institute of Advanced Engineering and Science (IAES)
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.