Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3
Key Confirmation in Key Exchange: A Formal Treatment and Implications for TLS 1.3
复制标题
密钥交换中的密钥确认：TLS 1.3 的正式处理和启示
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
B. Warinschi
中科院分区：
文献类型：
--
作者：
M. Fischlin;Felix Günther;Benedikt Schmidt;B. Warinschi
密钥交换协议允许远程位置的双方计算共享密钥。这类协议的共同安全概念是保密性和真实性，但许多广泛部署的协议和标准将另一个属性称为密钥确认作为主要设计目标。此属性应保证密钥交换协议中的一方确信另一方也持有共享密钥。值得注意的是，虽然保密性和真实性的定义已经得到了广泛的研究，但到目前为止，关键确认的处理却相当非正式。在这项工作中，我们提供了第一个严格的形式化的密钥确认，利用基于游戏的安全框架，建立了密钥交换的保密和认证概念。我们定义了两种口味的密钥确认，充分和几乎充分的密钥确认，考虑到不可避免的不对称的各方的角色相对于最终协议消息的传输。这些概念捕获了密钥交换的两个通信伙伴合理预期的最强级别的密钥确认。我们证明了具有精确的安全定义的密钥确认的好处，将它们应用到下一个版本的传输层安全（TLS）协议，版本1.3，目前由互联网工程任务组（IETF）开发。我们的分析表明，TLS 1.3草案draft-ietf-tls-tls 13 -10中规定的完全握手实现了客户端和服务器的密钥确认的理想概念。虽然密钥确认通常被理解，并且在TLS 1.3草案中被描述为从交换的完成消息中获得，但有趣的是，我们可以证明，即使没有这些消息，完整的TLS 1.3握手也提供了密钥确认，从而正式阐明了不同握手消息所带来的安全属性。我们进一步证明了严格的定义的有用性，通过重新审视民间传说的方法来建立关键的确认（如在NIST的SP 800- 56 A中讨论的）。我们提供了一个形式化作为一个通用的协议转换，并表明所产生的协议享有强大的密钥确认保证，从而确认其有益的使用在理论和实际的协议设计。
Key exchange protocols allow two parties at remote locations to compute a shared secret key. The common security notions for such protocols are secrecy and authenticity, but many widely deployed protocols and standards name another property, called key confirmation, as a major design goal. This property should guarantee that a party in the key exchange protocol is assured that another party also holds the shared key. Remarkably, while secrecy and authenticity definitions have been studied extensively, key confirmation has been treated rather informally so far. In this work, we provide the first rigorous formalization of key confirmation, leveraging the game-based security framework well-established for secrecy and authentication notions for key exchange. We define two flavors of key confirmation, full and almost-full key confirmation, taking into account the inevitable asymmetry of the roles of the parties with respect to the transmission of the final protocol message. These notions capture the strongest level of key confirmation reasonably expectable for the two communication partners of the key exchange. We demonstrate the benefits of having precise security definitions for key-confirmation by applying them to the next version of the Transport Layer Security (TLS) protocol, version 1.3, currently developed by the Internet Engineering Task Force (IETF). Our analysis shows that the full handshake as specified in the TLS 1.3 draft draft-ietf-tls-tls13-10 achieves desirable notions of key confirmation for both clients and servers. While key confirmation is generally understood and in the TLS 1.3 draft described as being obtained from the Finished messages exchanged, interestingly we can show that the full TLS 1.3 handshake provides key confirmation even without those messages, shedding a formal light on the security properties different handshake messages entail. We further demonstrate the usefulness of rigorous definition by revisiting a folklore approach to establish key confirmation (as discussed for example in SP 800-56A of NIST). We provide a formalization as a generic protocol transformation and show that the resulting protocols enjoy strong key confirmation guarantees, thus confirming its beneficial use in both theoretical and practical protocol designs.