| 基于进程代数的TCG远程证明协议的形式化验证 |
| |
| 引用本文： | 王勇,方娟,任兴田,林莉. 基于进程代数的TCG远程证明协议的形式化验证[J]. 计算机研究与发展, 2013, 50(2): 325-331 |
| |
| 作者姓名： | 王勇 方娟 任兴田 林莉 |
| |
| 作者单位： | 北京工业大学计算机学院 北京 100124 |
| |
| 基金项目： | 国家“九七三”重点基础研究发展计划基金项目(2007CB311100);北京市教委科技计划基金项目(JC007011201004);北京市人才强教中青年骨干培养基金项目 |
| |
| 摘 要： | 可信计算组织(Trusted Computing Group,TCG)的远程证明协议是最早提出的远程证明的解决方案,其协议的形式化验证对于工程实施具有重要意义.分析了TCG远程证明协议的两种形式——直接证明协议和借助可信第三方的证明协议,对它们进行了抽象处理,得到了两种协议形式的抽象模型.在抽象模型的基础上,给出了基于进程代数的形式化描述,并分别进行了形式化验证,验证结果表明两种协议形式的并行系统均展示了期望的外部行为.
|
| 关 键 词： | 可信计算 远程证明 协议验证 形式化 进程代数 |
Formal Verification of TCG Remote Attestation Protocols Based on Process Algebra |
| |
| Wang Yong , Fang Juan , Ren Xingtian , Lin Li. Formal Verification of TCG Remote Attestation Protocols Based on Process Algebra[J]. Journal of Computer Research and Development, 2013, 50(2): 325-331 |
| |
| Authors: | Wang Yong Fang Juan Ren Xingtian Lin Li |
| |
| Affiliation: | (College of Computer Science & Technology, Beijing University of Technology, Beijing 100124) |
| |
| Abstract: | |
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
