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

摘要

为了对可信平台控制模块的信任链建立过程进行理论验证,在对基于可信平台控制模块( 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.