基于串空间的可信计算协议分析

被引：16

作者：

冯伟 ^{[1
,2
]}

冯登国 ^{[1
]}

机构：

[1] 中国科学院软件研究所可信计算与信息保障实验室

[2] 中国科学院大学

来源：

计算机学报 | 2015年 / 38卷 / 04期

关键词：

可信计算; 远程证明; 串空间; 认证测试; 形式化验证;

D O I：

暂无

中图分类号：

TP309 [安全保密];

学科分类号：

081206 [计算机网络与安全];

摘要：

可信计算技术能为终端、网络以及云计算平台等环境提供安全支撑,其本身的安全机制或者协议应该得到严格的形式化证明.该文基于串空间模型对其远程证明协议进行了分析.首先,扩展了串空间的消息代数和攻击者串,使其能表达可信计算相关的密码学操作,并对衍生的定理进行了证明;并且提出了4个新的认证测试准则,能对协议中的加密、签名、身份生成和哈希等组件进行推理.其次,基于扩展的串空间模型对远程证明协议的安全属性(隐私性、机密性和认证性)进行了抽象和分析.最后,给出了对发现攻击的消息流程,并基于ARM开发板对其中的布谷鸟攻击进行了实现,验证了串空间的分析结果.

引用

页码：701 / 716

页数：16

共 6 条

[1]

可信计算技术研究 [J].