A comprehensive formal security analysis and revision of the two-phase key exchange primitive of TPM 2.0
A comprehensive formal security analysis and revision of the two-phase key exchange primitive of TPM 2.0
复制标题
TPM 2.0 两阶段密钥交换原语的全面形式安全分析和修订
DOI：
10.1016/j.comnet.2020.107369
复制
发表时间：
2019-06
影响因子：
5.6
通讯作者：
Shijun Zhao
中科院分区：
文献类型：
--
作者：
Qianying Zhang;Shijun Zhao
可信协议2.0版提供了两阶段密钥交换原语，可用于实现三种广泛标准化的认证密钥交换协议：完全统一模型、完全MQV和SM 2密钥交换协议。然而，在所有这些协议中都发现了漏洞。幸运的是，TPM芯片提供的保护似乎可以减轻这些漏洞。本文提出了一个安全模型，该模型能够捕获TPM对密钥和协议计算环境的保护，并且能够对多个协议进行统一分析。在统一安全模型的基础上，首次对TPM 2.0的密钥交换原语进行了形式化的安全分析，分析结果表明，在TPM芯片的硬件保护下，密钥交换原语确实满足我们的安全模型中定义良好的安全性质，但在一些不切实际的限制条件下，这将阻止密钥交换原语在真实世界网络中的应用。为了使TPM 2.0适用于现实网络，我们提出了一个修改的TPM 2.0的密钥交换原语，它可以是安全的，没有限制条件。我们给出了一个严格的分析，结果表明，我们的修改不仅达到了现代AKE安全模型的基本安全性质，但也有一些进一步的安全性质。
The Trusted Platform Module (TPM) version 2.0 provides a two-phase key exchange primitive which can be used to implement three widely-standardized authenticated key exchange protocols: the Full Unified Model, the Full MQV, and the SM2 key exchange protocols. However, vulnerabilities have been found in all of these protocols. Fortunately, it seems that the protections offered by TPM chips can mitigate these vulnerabilities. In this paper, we present a security model which captures TPM’s protections on keys and protocols’ computation environments and in which multiple protocols can be analyzed in a unified way. Based on the unified security model, we give the first formal security analysis of the key exchange primitive of TPM 2.0, and the analysis results show that, with the help of hardware protections of TPM chips, the key exchange primitive indeed satisfies the well-defined security property of our security model, but unfortunately under some impractical limiting conditions, which would prevent the application of the key exchange primitive in real-world networks. To make TPM 2.0 applicable to real-world networks, we present a revision of the key exchange primitive of TPM 2.0, which can be secure without the limiting conditions. We give a rigorous analysis of our revision, and the results show that our revision achieves not only the basic security property of modern AKE security models but also some further security properties.
登录
查看更多内容
DOI：
10.1007/978-3-319-22846-4_3
发表时间：
2015-08
期刊：
IACR Cryptol. ePrint Arch.
影响因子：
--
作者：
Shijun Zhao;Qianying Zhang
通讯作者：
Shijun Zhao;Qianying Zhang
DOI：
--
发表时间：
1986-02
期刊：
Transactions of the Institute of Electronics and Communication Engineers of Japan. Section E
影响因子：
--
作者：
Tsutomu Matsumoto;Y. Takashima;H. Imai
通讯作者：
Tsutomu Matsumoto;Y. Takashima;H. Imai
DOI：
10.1007/978-3-540-76900-2_29
发表时间：
2007-12
期刊：
--
影响因子：
--
作者：
T. Okamoto
通讯作者：
T. Okamoto
DOI：
10.1109/euc.2010.98
发表时间：
2010-12
期刊：
2010 IEEE/IFIP International Conference on Embedded and Ubiquitous Computing
影响因子：
--
作者：
Liqun Chen;B. Warinschi
通讯作者：
Liqun Chen;B. Warinschi
DOI：
10.1007/978-3-319-17533-1_11
发表时间：
2015-05
期刊：
IACR Cryptol. ePrint Arch.
影响因子：
--
作者：
Shijun Zhao;Qianying Zhang
通讯作者：
Shijun Zhao;Qianying Zhang