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

摘要：

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

关键词：可信计算、远程证明、串空间、认证测试、形式化验证

所属期刊栏目：38

分类号：TP309(计算技术、计算机技术)

资助基金：国家自然科学基金61202414,91118006;国家“九七三”重点基础研究发展规划项目基金2013CB338003;This work is partly supported by the National Natural Science Foundation of Chinaunder Grant .91118006 and 61202414;the National Basic Research Program 973 Program of Chinaunder Grants 2013CB338003

在线出版日期：2015-06-26（万方平台首次上网日期，不代表论文的发表时间）

页数：共16页

页码：701-716