可信计算中信任链建立的形式化验证  

Formal Verification of Establishment of Chain of Trust in Trusted Computing

作　　者：王勇[1] 许荣强[1] 任兴田[1] 杨建红[1] 

机构地区：[1]北京工业大学计算机学院,北京100124

出　　处：《北京工业大学学报》2016年第3期387-392,共6页Journal of Beijing University of Technology

基　　金：国家"973"计划资助项目(2007CB311100)

摘　　要：为了对可信平台控制模块的信任链建立过程进行理论验证,在对基于可信平台控制模块(trusted platform control module,TPCM)的信任链建立过程进行抽象处理的基础上,给出了抽象模型中各个实体状态的进程代数描述,并利用进程代数的公理系统做了形式化验证.验证的结果表明系统具有期望的外部行为.For formal verification for establishment of chain of trust, the process algebra description of each entity's state transferring was given based on the abstraction of the establishing process of trusted platform control modeule ( TPCM )-based chain of trust. Formal verification was conducted by use of axioms of process algebra. Verification result exhibits that the system has desired external behavior.

关 键 词：可信计算 信任链 可信平台控制模块 形式化验证 进程代数 

分 类 号：TP309.1[自动化与计算机技术—计算机系统结构]