可信计算技术通过从体系架构上建立攻击免疫机制，实现计算平台安全、可信赖运行。可信计算技术目前已经得到了普遍应用。随着可信计算技术的发展，其应用已经扩展到了新的平台与应用环境，并成为其重要发展趋势。目前已有的可信计算规范体系在应对新的应用和安全需求方面有所不足。为此，国际可信计算联盟组织在2013年发布了可信平台模块（Trusted Platform Module，简记为TPM）2.0标准，标志着下一代可信计算体系将要到来。因此，对下一代可信计算协议的研究成为当前可信计算领域的重要研究课题。　　本文致力于下一代可信计算协议的设计与分析的研究。首先利用形式化分析方法和自动分析技术，对下一代可信计算安全芯片的接口进行分析。然后，基于下一代可信计算安全芯片的安全功能，研究可信匿名认证协议的分析与设计。最后，结合安全芯片接口分析的状态特性，进一步研究和改进有状态协议的形式化分析方法。本文已取得的主要研究成果如下:　　1.建立了一类安全接口分析模型，对TPM2.0标准的授权机制进行了接口分析。在HMAC授权机制分析方面，本文建立了一个分析授权会话接口命令的机密性和认证性的威胁模型，并依据实际应用中会话密钥泄露的攻击场景对模型进行了实例化。随后，本文自动化给出了模型的中间人攻击，并对改进方案进行了形式化验证。在策略授权机制分析方面，本文利用有状态的应用π演算方法建立了一个通用的安全接口分析模型，并用该模型给出了策略授权机制的接口分析模型和安全属性形式化定义，以及该机制易被忽略的误用问题。随后，本文使用tamarin证明器对其进行了形式化验证，并发现三种误用情形，其中一种导致了对一个基于TPM2.0芯片构造的eID方案的实际攻击。　　2.提出了一种新的密钥管理接口的类型系统分析方法，并用其对TPM2.0标准的密钥管理接口进行了形式化验证。本文首先给出一种命令式语言适用于建模密钥管理的应用编程接口（Application Programming Interface，简记为API），并给出其机密性定义。随后，本文设计了一个类型系统，可以通过静态类型检查验证密钥管理接口的安全性。该类型系统允许为非对称密码学原语赋予类型。最后，本文利用该类型系统对TPM2.0标准的密钥管理接口进行了建模和类型检查，证明了其安全性。　　3.分析并设计了无可信第三方的基于信誉和撤销的可信匿名认证方案。本文分析发现并修正了此前无可信第三方的基于信誉系统和黑名单机制的匿名凭证方案BLACR中存在的重放攻击。同时，本文还发现另一个基于信誉系统的匿名认证方案PE(AR)2存在不正确的信誉的问题，且安全模型定义存在漏洞。为此，本文设计了一个可信匿名认证方案DAA-(AR)2。该方案利用TPM2.0标准的直接匿名证明（Direct Anonymous Attestation，简记为DAA）相关接口提供的安全功能在保证匿名性的条件下提升了信誉系统的安全性。本文还提出了一个基于模拟器的安全模型，保证方案的认证性、匿名性和不可陷害性，并在该模型中证明DAA-(AR)2方案是安全的。　　4.证明了两种有状态的应用π演算形式化方法的计算可靠性结论。本研究工作的安全性证明建立在可扩展的计算可靠性证明工具(Computational Soundness Proof，简记为CoSP)框架内。本文通过将有状态协议中的显式非单调状态嵌入CoSP协议的方式，分别证明了SAPIC演算和StatVerif演算这两种有状态的应用π演算形式化方法的计算可靠性结论。此外，本文给出SAPIC演算编码StatVerif演算的方法，从而首次获得两种语言之间的语义归约关系。本文的工作继承了CoSP工具的模块化证明特性，允许扩展加入任意在CoSP框架中已证明的具体的密码学原语。因此，本文针对一个具体的符号模型，证明了SAPIC和StatVerif工具计算可靠的自动化验证的结论。该符号模型包含了公钥加密和签名原语。　　总的来说，本文对下一代可信计算协议设计和分析理论与方法进行了深入研究。本文的研究成果为可信计算安全协议的分析建立了坚实的理论基础，并为可信计算安全协议的设计提供了有益参考。