| 基于串空间的可信计算协议分析 |
| |
| 引用本文： | 冯伟,冯登国.基于串空间的可信计算协议分析[J].计算机学报,2015,38(4). |
| |
| 作者姓名： | 冯伟 冯登国 |
| |
| 作者单位： | 1. 中国科学院软件研究所可信计算与信息保障实验室 北京 100190;中国科学院大学 北京100190
2. 中国科学院软件研究所可信计算与信息保障实验室 北京 100190 |
| |
| 基金项目： | 国家自然科学基金，国家“九七三”重点基础研究发展规划项目基金，This work is partly supported by the National Natural Science Foundation of China，the National Basic Research Program (973 Program) of China |
| |
| 摘 要： | 可信计算技术能为终端、网络以及云计算平台等环境提供安全支撑,其本身的安全机制或者协议应该得到严格的形式化证明.该文基于串空间模型对其远程证明协议进行了分析.首先,扩展了串空间的消息代数和攻击者串,使其能表达可信计算相关的密码学操作,并对衍生的定理进行了证明;并且提出了4个新的认证测试准则,能对协议中的加密、签名、身份生成和哈希等组件进行推理.其次,基于扩展的串空间模型对远程证明协议的安全属性(隐私性、机密性和认证性)进行了抽象和分析.最后,给出了对发现攻击的消息流程,并基于ARM开发板对其中的布谷鸟攻击进行了实现,验证了串空间的分析结果.
|
| 关 键 词： | 可信计算 远程证明 串空间 认证测试 形式化验证 |
Analyzing Trusted Computing Protocol Based on the Strand Spaces Model |
| |
| FENG Wei,FENG Deng-Guo.Analyzing Trusted Computing Protocol Based on the Strand Spaces Model[J].Chinese Journal of Computers,2015,38(4). |
| |
| Authors: | FENG Wei FENG Deng-Guo |
| |
| Abstract: | |
| |
| Keywords: | trusted computing remote attestation strand spaces authentication test formal verification |
| 本文献已被 万方数据 等数据库收录！ |
|
