Formal Security Analysis on Trusted Platform Module Based on Applied π Calculus

Trusted computing is a popular paradigm to enable computers to achieve a greater level of security than is possible in software alone. The core hardware component, named trusted platform module (TPM), is designed to achieve this goal. As there are many relevant products on the market and some attacks have already been found, it is very necessary to carry out the security analysis of TPM. However, because TPM is a complex security component whose specification is too long to be completely covered, the existing work hasnt formally or fully analyzed the issues about the various security properties. An applied π calculus model of the interactive processes between TPM and its user is proposed as a solid foundation for discussing the various security properties. Based on the formal model, the secrecy, authentication and weak secrecy problems of TPM are identified and formalized, some known attacks are rediscovered and some new attacks are found via a formal way rather than descriptions in natural language. Furthermore, the fixing proposals for the corresponding security vulnerabilities are presented and verified. In order to make the analysis and verification more accurate and efficient, the automatic theorem proving tool is also used during the analysis and verification.