A Formal Security Analysis Method of Application Programming Interfaces for Trusted Platform Module
Shiwei Xu · Journal of Wuhan University · 2010
Trusted Platform Module (TPM) which is the root of trusted computing provides the cryptographic functions through the Application Programming Interface (API). However the API is defined as un-formal description in TCG’s specification and the security policies are not discussed and guaranteed by TCG. We propose a formal model to describe the APIs system based on specification. In order to automatically verify the security policies,a formal deduction model based on resolution principle and theorem proving is presented,and a mechanism of executability determination is also integrated in the method to alleviate state space explosion problem to some extent. The proposed theory and method are then applied in the Key Migration module of TPM APIs and several design faults are disclosed.