基于条件谓词逻辑的可信计算形式化分析

随着可信计算应用的不断发展，针对可信计算的形式化分析理论将成为可信计算领域研究的热点。在深入研究可信计算相关技术、信任链建立和信任传递过程影响因素的基础上，提出了基于条件谓词逻辑的可信计算形式化分析方法。通过定义不同的谓词和推演规则，并在谓词逻辑中添加可信性的影响因素作为约束条件，实现对可信计算信任模型的形式化验证。利用提出的方法举例对可信计算平台安全引导过程进行了分析，并且根据分析结果提出了委托受限的安全引导过程。结果表明，基于条件谓词逻辑的形式化验证方法，能够清晰、有效的实现对可信计算信任模型的形式化分析，为可信计算应用模型的设计和完善提供参考。形式化方法的提出，对于丰富可信计算信任评估理论，促进可信计算应用发展具有一定的意义。

Formal Analysis of Trusted Computing Based on Conditional Predicate Logic

With the development of trusted computing application, Research on formal analysis to trusted computing will become a hot research field. Formal analysis method of trusted computing based on conditional predicate logic was proposed after studying the technologies of trusted computing, chain of trust and trust transfer. Trusted computing models can be evaluated with the predicates and inference rule defined here. Moreover, the influence factors to trust were added in predict logic as constraint conditions, which achieve the goal to depict trust relation more clearly. Secure bootstrap of trusted computing was analyzed with the proposed method, and a constrained secure bootstrap was proposed. Analyzing results show that trusted computing system can be clearly and effectively analyzed with the formal analysis method, which can provide assistance for designing and improving trusted computing model. The proposed method is important to enrich the evaluation theory and promote the application development of trusted computing.