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

Analyzing Trusted Computing Protocol Based on the Strand Spaces Model

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

Trusted Computing technology can provide security supports for terminals, networks and cloud computing platforms; and its secure mechanisms or protocols should be proved formally and rigorously. This paper tries to analyze its remote attestation protocol based on the strand spaces model. Firstly, we extend the term algebra and penetrator＇s model in the strand spaces in order to express the cryptographic operations used in trusted computing, and the derived theorems have also been proved. We also propose four new authentication test principles accordingly, which can be used to reason about the encryption, signature, identity-making and hash compo- nents in the protocol Then, we use the extended strand spaces model to describe and analyze the security properties （including privacy, secrecy and authentication） of remote attestation protocol. Finally, we describe the message flow of the attacks captured by the strand space analysis, and implement the cuckoo attack using ARM development board, which experimentally proved the results inferred from strand spaces model.