Key Confirmation in Key Exchange Protocols: Formal Definitions and Implications for TLS 1.3

Marc Fischlin, Felix Günther, Benedikt Schmidt, Bogdan Warinschi

Research output: Chapter in Book/Report/Conference proceedingConference Contribution (Conference Proceeding)

13 Citations (Scopus)

Abstract

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.
Original languageEnglish
Title of host publication2016 IEEE Symposium on Security and Privacy (S&P 2016)
Subtitle of host publicationProceedings of a meeting held 22-26 May 2016, San Jose, California, USA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Pages452-469
Number of pages18
ISBN (Electronic)9781509008247
ISBN (Print)9781509008254
DOIs
Publication statusPublished - Aug 2016

Publication series

Name2016 IEEE Symposium on Security and Privacy (SP)
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
ISSN (Print)2375-1207

Fingerprint Dive into the research topics of 'Key Confirmation in Key Exchange Protocols: Formal Definitions and Implications for TLS 1.3'. Together they form a unique fingerprint.

Cite this