A Theory of Matching Sessions

Authenticated Key Exchange protocols (AKEs) are cryptographic protocols that allow two or more parties to jointly compute a shared session key over an insecure public channel. This key can subsequently be used as input to other algorithms in order to provide various secure services for and between said parties. Ever since the advent of provable security, an enormous amount of research has been done to define ever-stronger complexity-theoretic security models to capture desirable AKE properties. However, consensus has yet to be established over which models are the most suitable, both in theory and practice. Several modelling artefacts are at the heart of this problem. First of all, provable security has not yet yielded a unified definition for what it means for parties running a protocol to have established matching sessions. Many different ad hoc avenues have been proposed to deal with this (matching conversations, pre-established or post-established sessions identities, matching functions, etc.) but they often introduce artificial subtleties that yield incompatibility results between models that seem otherwise acceptable. Secondly, a fundamental definition of internal state information is also lacking; this introduces even more difficulties in comparing models that authorize the attacker to obtain various forms of this internal state (unerased internal state revealing, session state revealing, ephemeral key revealing, etc.). Furthermore, internal state revealing seems to be widely more-or-less hard to deal with depending on the model’s underlying flavor, i.e., whether it is indistinguishability-based or simulation-based. We strongly believe that the above-mentioned discrepancies rest on something that is fundamentally unified, and with this proposal we wish to undertake the tasks of 1) discovering and studying this mathematical lowest common denominator and 2) using the outcome of this study to find some order in the vast landscape that is AKE security modelling, and uncover the core governing observed incompatibility results. Our goal is to conduct this study 1) independently of the authentication mechanism used (PKI-based, password-based, attribute-based, etc…) and 2) independently the underlying intractability assumption (group-based, lattice-based, quantum-based etc.). Incorporating quantum key distribution to the study is particularly promising because the interface between the quantum phase and the classical phase within such protocols is highly under-investigated. Furthermore, the threat models in which quantum proofs of security are established are not clearly defined. How to solve these problems will certainly bring further insight to AKE security modelling as a whole.