Using First Order Logic to Reason about TCG´s TPM Specification

Trusted Platform Module (TPM) provides the cryptographic functions through the Application Programming Interfaces (APIs). The specification of APIs reflects the security policies of the designers, in order to manage and protect the sensitive information of users, which is stored in the hardware module. But the security of these APIs has not guaranteed. In this paper, a formal model to describe the APIs based on the specification is proposed; based on the model, the attacker ability and the system security target are defined. In order to find the API-chain attack automatically, a formal method based on resolution principle and theorem proving is presented, and the method takes in practical using an automata theorem prover Otter; a mechanism of executability determination is also integrated in the method to alleviate state space explosion problem to some extent, and the state of TPM can be guaranteed. The proposed theory and method are then applied in the Key Migration Module of TPM APIs to show the feasibility of this method.