基于进程代数的TCG远程证明协议的形式化验证

Formal Verification of TCG Remote Attestation Protocols Based on Process Algebra

可信计算组织(Trusted Computing Group,TCG)的远程证明协议是最早提出的远程证明的解决方案,其协议的形式化验证对于工程实施具有重要意义.分析了TCG远程证明协议的两种形式——直接证明协议和借助可信第三方的证明协议,对它们进行了抽象处理,得到了两种协议形式的抽象模型.在抽象模型的基础上,给出了基于进程代数的形式化描述,并分别进行了形式化验证.验证结果表明两种协议形式的并行系统均展示了期望的外部行为.

Remote attestation protocol of TCG （Trusted Computing Group） is the earliest remote attestation solution for trusted computing. Two forms of TCG remote attestation are analyzed： direct remote attestation protocol and remote attestation with trusted third party protocol. And the abstract models of the above two forms are presented in which interacting channels between the whole system and the outside environment are treated as exterior channels and interacting channels between parts of the system are treated as inner channels. Based on these abstract models, we provide the process algebra-based formal descriptions, in which every part involved in the protocols is described by a process term to capture the state transitions of the system part, and we put these process terms into parallel to get the whole formal systems. Then we conduct the related formal verifications of the parallel formal system based on the axioms of process algebra. The verification results show that the formal systems of two protocols exhibit desired external behaviors.