Security analysis of SPAKE2+

We show that a slight variant of Protocol SPAKE2 +, which was presented but not analyzed in [17], is a secure asymmetric password-authenticated key exchange protocol (PAKE), meaning that the protocol still provides good security guarantees even if a server is compromised and the password file stored on the server is leaked to an adversary. The analysis is done in the UC framework (i.e., a simulation-based security model), under the computational Diffie-Hellman (CDH) assumption, and modeling certain hash functions as random oracles. The main difference between our variant and the original Protocol SPAKE2 + is that our variant includes standard key confirmation flows; also, adding these flows allows some slight simplification to the remainder of the protocol. Along the way, we also (i) provide the first proof (under the same assumptions) that a slight variant of Protocol SPAKE2 from [5] is a secure symmetric PAKE in the UC framework (previous security proofs were all in the weaker BPR framework [7]); (ii) provide a proof (under very similar assumptions) that a variant of Protocol SPAKE2 + that is currently being standardized is also a secure asymmetric PAKE; (iii) repair several problems in earlier UC formulations of secure symmetric and asymmetric PAKE.