摘要

可信计算是一种经典的系统安全技术，在保障国家网络空间安全方面具有重要的作用。随着移动计算、物联网等新型计算平台的出现，国际可信计算组织发布了支持这些新型计算平台的下一代 TPM 规范，即 TPM 2.0。与 TPM 1.2 相比，新的 TPM 2.0 规范在密码学操作原语 API、授权协议以及应用灵活性等各个方面都有很多改进与提升。之前很多研究工作都是针对 TPM 1.2 的安全性进行分析，而 TPM 2.0 新增改进的功能还缺少相应的分析方法；为此，本文重点研究在 TPM 2.0 中新增和改进功能模块的安全性，以及基于 TPM 2.0 功能模块所能实现协议的设计与分析研究。基于 TPM 2.0 的协议设计与分析研究主要包含两条研究主线：其一是 TPM 2.0 协议和接口的形式化分析方法研究；其二是TPM 2.0 协议及匿名认证协议的设计和应用研究。这两个方面的研究是相辅相成的，对 TPM 2.0 协议的形式化分析研究能够促进协议的改进与完善，而对协议的设计改进与应用研究又能反过来促进形式化模型更加精确。因此，基于 TPM 2.0的协议设计与分析工作主要从三个方面展开：安全协议形式化理论与分析、基于 TPM 2.0 的基础协议和接口的安全性分析以及可信计算延伸协议的设计与形式化分析。本文已经取得的主要研究成果如下：

(1) 完成基于 HMAC 的 TPM 2.0 授权协议的自动化证明。使用基于计算模型的证明工具 CryptoVerif 证明了 TPM 2.0 授权协议的安全性，它的方法采用基于游戏序列的证明技术，这些游戏由一种概率多项式时间的进程演算的语言来表述。首先，使用概率多项式进程演算对 TPM 2.0 的授权协议建模，并提出对应性（correspondence 属性）作为授权协议的一个更加通用的安全目标；然后，使用 CryptoVerif 工具自动证明 TPM 2.0 授权协议中的对应性。证明结果表明计算模型下 TPM 2.0 授权协议的认证性成立。

(2) 提出了一个分析 TPM 2.0 密码支撑命令的通用形式化模型。该形式化模型支持密钥创建和删除、密钥导出、对称加密、非对称加密、消息认证码、签名等操作。模型建立过程中考虑了密钥的类型和简单的属性，并且提出在现代密码学概念下的安全属性，利用自动证明工具证明了在现代密码学假设下的安全性。该模型具有广泛的通用性和普适性，除了适用于分析 TPM 2.0 的命令，还能分析PKCS#11 等的密码学 API。

(3) 改进并设计了一种匿名认证协议。匿名认证协议保证证明方能够向验证方证明自己合法的身份信息，但又避免暴露自己真实的身份信息。匿名认证是TPM 2.0 在隐私认证方面的一个重要特征（如 TPM 2.0 支持的 DAA 协议）。通过研究一系列匿名认证协议及其黑名单撤销机制实现的过程后，发现了匿名认证协议存在的一些不足与漏洞：匿名认证系统 BLACR 在启用快速通道认证时，不支持移出奖励名单和惩罚名单的功能； BLACR 快速通道令牌存在重放攻击安全漏洞。本文提出了 ExBLACR 方案，对存在的问题进行了改进，并解决了重放攻击问题。

(4) 提出了针对无可信第三方黑名单匿名认证协议的形式化分析方法。首先，使用应用 Pi 演算给出了在符号模型下 BLAC 类系统的一些通用安全属性的定义；然后，将这些定义表示为适合形式化分析工具可验证的对应性（correspondence，包含认证性, 不可陷害性和抗误认证性）以及等价性（equivalence，包含匿名性和不可链接性）。本文在 BLACR 系统中验证了这些安全属性，在分析中发现了快速通道认证令牌机制的一个已知攻击；并针对性地提出了一个安全修订，使得该令牌机制能够成功通过 ProVerif 的验证。

总的来说，本文对可信计算最新 TPM 2.0 规范的相关协议和接口进行了深入分析与研究。相关研究成果为 TPM 2.0 技术的应用推广提供了科学的理论基础和严谨的技术验证，并为可信计算协议的进一步发展与改进提供了有益参考。

                                                         Abstract

Trusted Computing is a classic technology for system security, and plays an important role in guaranteeing the security of national cyberspace. With the emergence ofnew computing platforms such as mobile computing and the Internet of Things (IoT),TCG (Trusted Computing Group) has released the next-generation TPM specification(called TPM 2.0) that supporting these new computing platforms. Compared to the traditional TPM 1.2, there are many improvements in the new TPM 2.0 specification, such as cryptographic operations, authorization protocols and application flexibility. Previous work mainly aimed at the security analysis of TPM 1.2, and the analysis methodsfor the new and improved features in TPM 2.0 are lack. Thus, this thesis focuses on the security of the new and improved functional modules in TPM 2.0, as well as the design and analysis of protocols that can be implemented based on TPM 2.0. The protocol design and analysis based on TPM 2.0 mainly includes two research main lines: one is the formal analysis method of TPM 2.0 protocols and interfaces; the second is the design and application research of TPM 2.0 protocols (especially, the anonymous attestation protocols). These two aspects of research are mutually reinforcing, the formal analysis methods can promote the improvement of the TPM 2.0 protocols, and the design improvement and application research of the protocols can in turn makes the formal model more accurate. Therefore, this thesis is dedicated to research on the design and analysis of the TPM 2.0 protocols and API interfaces. The work is mainly carried out in three aspects: the formalization theory and analysis of security protocols, the security analysis of basic protocols and interfaces based on TPM 2.0, and the design and formal analysis of trusted computing extension protocols (like anonymous credentials). The main contributions of this thesis are as follows:

(1) The thesis has finished the automated proof of HMAC-based authorization protocol in the TPM 2.0. The security of the authorization protocols in the TPM 2.0 are proved by using the tool CryptoVerif in the computational model. CryptoVerif builds proofs by sequences of games, and these games are expressed by a probabilistic polynomial-time calculus. First, we model the authorization protocols by using a probabilistic polynomial-time calculus, and propose correspondence property as a more general security goal. Then, we apply CryptoVerif to prove the correspondence properties of the authorization protocols in the TPM 2.0 automatically. The proof results show that the authentication of the authorization protocols of TPM 2.0 in the computational model is established.

(2) The thesis has proposed a general formal model for analyzing the cryptographic support commands in the TPM 2.0. The model supports many commands, such as key creations, key deletions, key exports, symmetric encryption, asymmetric encryption, message authentication code, signature, etc. The model also considers the key types and simple properties. We model these commands with a security policy expressed in the notion of modern cryptography, and prove that these commands satisfy this security policy by using an automated formal tool. The model has a wide range of versatility and universality, which is suitable for analyzing the commands and cryptographic APIs in both TPM 2.0 and PKCS11.

(3) The thesis has improved and designed a kind of anonymous attestation protocol. The anonymous attestation protocol guarantees that the prover can prove its legal identity to the verifier, but at the same time avoids exposing its true identity information. It is an important feature in the privacy authentication of TPM 2.0 (such as DAA protocols supported by TPM 2.0). After the study of a series of anonymous attestation protocols and their revocation mechanisms, we discovered some problems and vulnerabilities: the BLACR does not support unblacklisting when enabling the express lane tokens; the express lane tokens can be reused (replay attack). Thus, we propose ExBLACR method, which provides solutions to these problems, and can resist replay attack.

(4) The thesis has introduced a formal analysis method for the TTP-Free blacklistable anonymous credentials system. First, we give the definitions of some common security properties for BLAC-like systems in the symbolic model using applied pi calculus. Then, these definitions are expressed as correspondence properties (authenticity, non-frameability, and mis-authentication resistance) and equivalence properties (anonymity and unlinkability) that are suited to verify by formal analysis tool. We verify these properties in BLACR system, and finds a known attack aiming at the token mechanism in the express-lane authentication. Finally, we offer a security revision that makes the token mechanism be successfully proved by using ProVerif.

In summary, this thesis conducts a deep research and analysis for the related protocols and interfaces in the newest TPM 2.0 specification of trusted computing. The research results of this thesis provide a scientific theoretical foundation and a rigorous technical verification for the application and promotion of TPM 2.0 related technologies, and show a useful reference for the further development and improvement of trusted computing protocols.