Abstract:

A formalized analysis method of trusted computing is proposed based on conditional predicate logic which fomally verifies trusted computing models. In this method, different predicates and reasoning rules are defined, and the factors to influence the credibility are added in the predicate logic as constraint conditions. Thus, the trusted computing models are successfully verified. Moreover, the secure bootstrap process of the trusted computing plat- form is analyzed via an example, and a secure bootstrap process of the trusted computing platform with constrained delegation length is proposed. The results show that the proposed method can be clearly and effectively used for the formalized analysis of trusted computing models.

Key words: information security, trusted computing, trust chain, conditional predicate logic