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

• 作者: 任兴田 方娟 林莉 王勇
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: 可信计算 远程证明 协议验证 形式化 进程代数
• 年，卷（期）: 2013,（2）
• 所属期刊栏目: 计算机网络与信息安全
• 页码范围: 325-331
• 页数: 7页
• 分类号: TP309.1
• 字数: 3637字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	方娟	北京工业大学计算机学院	60	267	9.0	12.0
2	王勇	北京工业大学计算机学院	50	389	8.0	18.0
3	任兴田	北京工业大学计算机学院	12	65	5.0	7.0
4	林莉	北京工业大学计算机学院	7	25	4.0	4.0