Nearly Tight Diffie-Hellman-Based Key Exchange – A theoretical analysis of practical protocols

Abstract

Formålet med denne oppgaven er å beskrive og analysere flere Diffie-Hellman- baserte nøkkelutvekslingsprotokoller, med vekt på skarpe sikkerhetsbevis. Sentralt i analysen er et enkelt og praktisk Diffie-Hellman-basert protokoll basert på protokollet i [CCG+ 19]. For å analysere de Diffie-Hellman-baserte protokollene definerer vi en formell sikkerhetsmodell. Vi gir presise definisjoner på begreper som implisitt nøkkelautentisering (implicit key authentication) og svakt fremtidssikkert hemmelighold (weak forward secrecy). I de tilfellene der sikkerhet- skravene ikke oppnås, viser vi dette ved angrep mot protokollene. Deretter gir vi nesten skarpe reduksjoner som viser at protokollet basert på [CCG+ 19] er sikkert: her er analysen inspirert av analysen i [CCG+ 19], men bevisstrategien er annerledes. Til dette tar vi i bruk en form for “enveis”-variant av svakt fremtidssikkert hemmelighold, som vi viser at kan oppgraderes skarpt til svakt fremtidssikkert hemmelighold ved hjelp av tilfeldige orakler. Til sist definerer vi en form for eksplisitt nøkkelautentisering i den formelle modellen vår. Vi konstruerer et protokoll som oppnår denne formen for autentisering, ved en skarp reduksjon til “enveis”-sikkerheten i det underliggende protokollet. Dette gjør vi ved å ta i bruk nøkkelbekreftelsesmeldinger — bevisstrategien minner om den i [PRZ24].

In this thesis, we describe and analyze several Diffie-Hellman-based key exchange protocols, with an emphasis on giving tight security proofs. At the centre of our analysis is a simple and highly practical Diffie-Hellman-based protocol, similar to the one considered in [CCG+ 19]. To enable a formal analysis of key exchange security, we define a security model for key exchange, giving precise formal interpretations of notions such as implicit key authentication and weak forward secrecy. Using our formal model, we analyze the security of each protocol in turn. Where implicit key authentication and weak forward secrecy fail to hold, we give attacks to demonstrate it. We then proceed to give nearly tight reductions to show the security of the protocol based on [CCG+ 19]: the analysis is similar to that in [CCG+ 19], but the proof strategy employed borrows instead from [PRZ24]. Specifically, we consider a notion of one-way weak forward secrecy, which we show can be tightly upgraded to weak forward secrecy in the random oracle model. Finally, we define a notion of explicit key authentication with respect to our formal model, and construct a protocol for which explicit key authentication can be tightly reduced to the one-way weak forward secrecy of the underlying protocol, via the use of key confirmation messages. Again, the proof strategy is similar to that in [PRZ24].