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

被引：5

作者：

王勇

方娟

任兴田

林莉

机构：

[1] 北京工业大学计算机学院

来源：

计算机研究与发展 | 2013年 / 50卷 / 02期

关键词：

可信计算; 远程证明; 协议验证; 形式化; 进程代数;

D O I：

暂无

中图分类号：

TP309 [安全保密];

学科分类号：

081201 ; 0839 ; 1402 ;

摘要：

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

引用

页码：325 / 331

页数：7

共 7 条

[1] 可信计算的研究与发展 [J].