On Composability and Security of Game-based Password-Authenticated Key Exchange

The main purpose of Password-Authenticated Key Exchange (PAKE) is to allow secure authenticated communication over insecure networks between two or more parties who only share a low-entropy password. It is common practice that the secret key derived from a PAKE execution is used to authenticate and encrypt some data payload using symmetric key protocols. Unfortunately, most PAKEs of practical interest, including three protocols considered in this thesis, are studied using so-called game-based models, which -- unlike simulation models -- do not guarantee secure composition per se. However, Brzuska et al. (CCS 2011) have shown that a middle ground is possible in the case of authenticated key exchange that relies on Public-Key Infrastructure (PKI): the game-based models do provide secure composition guarantees when the class of higher-level applications is restricted to symmetric-key protocols. The question that we pose in this thesis is whether or not a similar result can be exhibited for PAKE. Our work answers this question positively. More specifically, we show that PAKE protocols secure according to the game-based Real-or-Random (RoR) definition of Abdalla et al. (PKC 2005) allow for automatic, secure composition with arbitrary, higher-level symmetric key protocols. Since there is evidence that most PAKEs secure in the Find-then-Guess (FtG) model of Bellare et al. (EUROCRYPT 2000) are in fact secure according to the RoR definition, we can conclude that nearly all provably secure PAKEs enjoy a certain degree of composition, one that at least covers the case of implementing secure channels. Although many different protocols that accomplish PAKE have been proposed over last two decades, only a few newcomers managed to find their way to real world applications - albeit lacking an intense and prolonged public scrutiny. As a step in the direction of providing one, this dissertation considers the security and efficiency of two relatively recently proposed PAKE protocols - Dragonfly and J-PAKE. In particular, we prove the security of a very close variant of Dragonfly employing the standard FtG model which incorporates forward secrecy. Thus, our work confirms that Dragonfly's main flows are sound. Furthermore, we contribute to the discussion by proposing and examining (in the RoR model of security) two variants of J-PAKE - which we call RO-J-PAKE and CRS-J-PAKE - that each makes the use of two less zero-knowledge proofs than the original protocol, at the cost of an additional security assumption. Our work reveals that CRS-J-PAKE has an edge in terms of efficiency over J-PAKE for both standard group choices: subgroups of finite fields and elliptic curves. The same is true for RO-J-PAKE, but only when instantiated with elliptic curves