中文摘要：

信任平台模块(TPM ) ，在物理资源上实现的一个系统部件，被设计使计算机能比独自由软件完成是可能的安全级别完成安全的高水平。为这个原因， TPM 提供一个方法在它的记忆存储密码的钥匙和另外的敏感数据，它从被除 TPM 以外的任何实体的存取被防护。想要使用那些钥匙和数据达到一些安全目标的用户被限制通过它在 TPM 说明定义的 API 与 TPM 交往。因此， TPM 是否能提供它宣称的保护的能力，取决于到大程度它的 API 的安全。在这份报纸，我们设计一个正式模型，它对充分使机械化的分析可存取，为在 TPM2.0 说明的关键管理 API。我们在我们的模型识别并且形式化然后成功地使用自动化证明器 Tamarin 获得他们的首先使机械化的分析这些 API 的安全性质。分析证明 TPM API 的关键管理子集为新鲜钥匙和柄的无界的数字保存非可加倍的钥匙的秘密。分析也报导关键复制机制，过去常复制在二个层次之间的一把钥匙，对扮演攻击脆弱，它使一个对手能恢复发源层次的复制钥匙或进口他的自己的钥匙进目的地层次。瞄准避免这些危险，我们建议一条途径，它限制发源和目的地 TPM 在复制期间证实对方身份。当他们被复制时，然后，我们正式证明我们的途径维持可加倍的钥匙的秘密。

英文摘要：

The trusted platform module （TPM）, a system component implemented on physical resources, is designed to enable computers to achieve a higher level of security than the security level that it is possible to achieve by software alone. For this reason, the TPM provides a way to store cryptographic keys and other sensitive data in its memory, which is shielded from access by any entity other than the TPM. Users who want to use those keys and data to achieve some security goals are restricted to interact with the TPM through its APIs defined in the TPM speci- fication. Therefore, whether the TPM can provide Pro- tected Capabilities it claimed depends to a large extent on the security of its APIs. In this paper, we devise a formal model, which is accessible to a fully mechanized analysis, for the key management APIs in the TPM2.0 specification. We identify and formalize security properties of these APIs in our model and then successfully use the automated prover Tamarin to obtain the first mechanized analysis of them. The analysis shows that the key management subset of TPM APIs preserves the secrecy of non-duplicable keys for unbounded numbers of fresh keys and handles. The analysis also reports that the key duplication mechanism, used to duplicate a key between two hierarchies, is vul- nerable to impersonation attacks, which enable an adver- sary to recover the duplicated key of the originating hierarchy or import his own key into the destination hier- archy. Aiming at avoiding these vulnerabilities, we proposean approach, which restricts the originating and destination TPMs to authenticate each other＇ s identity during duplication. Then we formally demonstrate that our approach maintains the secrecy of duplicable keys when they are duplicated.