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

• 作者: 冯伟 冯登国
• 来源期刊: 计算机学报
• 学科: 工学
• 关键词: 可信计算 远程证明 串空间 认证测试 形式化验证
• 年，卷（期）: 2015,（4）
• 所属期刊栏目: 信息安全
• 页码范围: 701-716
• 页数: 16页
• 分类号: TP309
• 字数: 19366字
• 语种: 中文
• DOI: 10.3724/SP.J.1016.2015.00701

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	冯登国	中国科学院软件研究所可信计算与信息保障实验室	243	6305	35.0	71.0
2	冯伟	中国科学院软件研究所可信计算与信息保障实验室	36	224	9.0	13.0