Authentication in Key-Exchange: Definitions, Relations and Composition

We present a systematic approach to define and study authentication notions in authenticated key-exchange protocols. We propose and use a flexible and expressive predicate-based definitional framework. Our definitions capture key and entity authentication, in both implicit and explicit variants, as...

Full description

Saved in:
Bibliographic Details
Main Authors: de Saint Guilhem, Cyprien Delpech, Fischlin, Marc, Warinschi, Bogdan
Format: Conference Proceeding
Language:English
Subjects:
Authentication
Computer science
Games
Protocols
Resistance
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present a systematic approach to define and study authentication notions in authenticated key-exchange protocols. We propose and use a flexible and expressive predicate-based definitional framework. Our definitions capture key and entity authentication, in both implicit and explicit variants, as well as key and entity confirmation, for authenticated key-exchange protocols. In particular, we capture critical notions in the authentication space such as key-compromise impersonation resistance and security against unknown key-share attacks. We first discuss these definitions within the Bellare-Rogaway model and then extend them to Canetti-Krawczyk-style models. We then show two useful applications of our framework. First, we look at the authentication guarantees of three representative protocols to draw several useful lessons for protocol design. The core technical contribution of this paper is then to formally establish that composition of secure implicitly authenticated key-exchange with subsequent confirmation protocols yields explicit authentication guarantees. Without a formal separation of implicit and explicit authentication from secrecy, a proof of this folklore result could not have been established.
ISSN:2374-8303
DOI:10.1109/CSF49147.2020.00028