下一代可信计算平台远程证明理论与方法研究

The remote attestation for next generation trust computing platform has already been becoming the research hotspot at home and abroad, which has great significance to solve the application problem in cloud server and terminal trust, mobile terminal security, digital right system, trust network connection, etc.. The research will makes the breakthroughs in key technology of remote attestation for next generation trust computing platform, study the model and protocol on the anonymous property attestation for TPM/TCM; It will study the security analysis verification for the correctness, anonymity and privacy by the method of integrating the cryptographic protocol proof with finite states machine verification; It will also develop a simulation testing tool for remote attestation, and optimize the protocol algorithms and parameters by the test and analysis. In a word, the research will make the studies on the remote attestation design, analysis and verification for next generation trust computing platform in the view of security argument and verification. It will not only lay the theory foundation of remote attestation system design and application for next generation trust computing platform, but also provide the tools supporting for the relative analysis and test.

下一代可信计算平台远程证明已成为目前国内外研究的热点，它在解决云计算终端和服务器信任、移动互联网终端安全、数字版权系统、可信网络接入等方面的应用有着现实重要意义。本课题重点突破下一代可信计算平台远程证明关键技术，研究基于 TPM/TCM安全芯片的匿名属性远程证明模型及其安全协议；采用密码协议证明和有限状态机自动化验证相结合的方法，进行远程证明的正确性、匿名性以及隐私性的安全性分析验证研究；同时还将研发一套远程证明协议仿真测试工具，通过安全性测试分析实现协议算法和参数的优化。总之，本课题从远程证明安全性论证和验证角度展开下一代远程证明协议的设计、分析和验证研究，不仅为下一代可信计算平台远程证明系统设计和应用奠定理论基础，还提供相应的分析验证、仿真检测工具支撑。

远程证明是可信计算核心关键技术，近年来已经成为重要的国内外研究热点。它主要用于解决终端平台间建立相互信任和网络信任的基础研究问题，在云服务器信任、物联网节点信任、嵌入式终端设备认证、可信网络接入控制等方面都有着广泛应用。本课题重点研究基于 TPM/TCM安全芯片的远程证明模型和方法；采用形式化分析方法验证远程证明协议的正确性、匿名性以及隐私性，并且构建仿真平台对远程证明方案的可用性及性能进行测试分析；并进一步将实用证明协议推广应用到移动可信计算、工业控制系统等应用领域，解决实际应用中的设备认证和可信环境验证等安全问题。.本课题在远程证明的直接匿名证明协议形式化分析和改进、移动嵌入式环境信任构建及证明、可信工控系统的远程证明和监控等方面取得一系列研究成果，特别是基于TPM2.0的远程证明协议安全分析和测试评估，高效远程证明应用方案设计等方面取得重要成果。.1）基于进程演算建立通用的直接匿名证明协议分析模型框架，采用ProVerif自动化分析工具对通用的DAA协议进行分析，发现其存在前向匿名性的安全隐患。.2）针对TPM 2.0的DAA接口进行安全分析，发现通过对接口参数的构造调用仍然存在Static DH oracle攻击，可将协议的安全强度降低2/3，该成果发表于Trust2014国际会议上，推动了TPM 2.0技术规范的修订。.3）研制的可信工控证明系统以国产自主可控的TCM芯片级的硬件安全为基础，采用“白名单”防护机制对工控系统终端实施主动防护。目前我们联合国内某工控企业将该系统已成功部署、应用到石化行业的工业控制系统中；针对新型的移动嵌入式平台提出MTM的可信体系架构，以及基于PUF实现了轻量级低端嵌入式设备的远程证明。.本课题共计发表SCI/EI国内外会议/期刊论文16篇，完成直接匿名证明协议仿真测试评估报告1份；申请国内专利3项，软件著作权3项，形成“可信计算直接匿名证明”密码行业标准草案1项。.本课题研究解决了下一代远程证明协议设计和分析的方法问题，针对TPM2.0协议和接口分析所取得的成果，大幅度提高了远程证明协议的安全性。新型移动嵌入式平台的远程证明方案的研究，推进了可信计算技术在云计算、物联网、移动互联网等领域的发展。我们研制的基于国产自主可信芯片的远程证明系统，目前已经应用于石化领域内的工控企业，这将极大的推进了下一代远程证明协议方案的实际应用。