Formal Analysis of Secure Bootstrap in Trusted Computing

摘要

The stated goal of the trusted computing is to redesign PC hardware for providing protection against software attack. Trust platform is key technology of trusted computing. However, the security of trusted platform should be verified in theory, and the model of trusted platform should be further improved. In this paper, a formal method for verifying the security of trusted platform is presented. The vulnerability of secure bootstrap is analyzed based on the proposed formal semantics. Moreover, an improved model of secure bootstrap is proposed. The semantics presented here also can be used to reasoning about other applications of trusted computing, which provides a general and effective method for analyzing security of trusted computing applications.