Michel Abdalla
email: michel.abdalla@ens.fr

Manuel Barbosa

Tatiana Bradley
email: tebradle@uci.edu

Stanis Law Jarecki

Jonathan Katz
email: jkatz2@gmail.com

Jiayu Xu

Universally Composable Relaxed Password Authenticated Key Exchange

Protocols for password authenticated key exchange (PAKE) allow two parties who share only a weak password to agree on a cryptographic key. We revisit the notion of PAKE in the universal composability (UC) framework, and propose a relaxation of the PAKE functionality of Canetti et al. that we call lazy-extraction PAKE (lePAKE). Our relaxation allows the ideal-world adversary to postpone its password guess until after a session is complete. We argue that this relaxed notion still provides meaningful security in the password-only setting. As our main result, we show that several PAKE protocols that were previously only proven secure with respect to a "game-based" definition of security can be shown to UC-realize the lePAKE functionality in the random-oracle model. These include SPEKE, SPAKE2, and TBPEKE, the most efficient PAKE schemes currently known.

Introduction

Protocols for password authenticated key exchange (PAKE) allow two parties who share only a weak password to agree on a cryptographically strong key by communicating over an insecure network. PAKE protocols have been studied extensively in the cryptographic literature [START_REF] Bellovin | Encrypted key exchange: Password-based protocols secure against dictionary attacks[END_REF][START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF][START_REF] Boyko | Provably secure password-authenticated key exchange using Diffie-Hellman[END_REF][START_REF] Goldreich | Session-key generation using human passwords only[END_REF][START_REF] Katz | Efficient password-authenticated key exchange using human-memorable passwords[END_REF][START_REF] Canetti | Universally composable password-based key exchange[END_REF][START_REF] Gennaro | Faster and shorter password-authenticated key exchange[END_REF], and are compelling given the widespread use of passwords for authentication. Even though the current practice is to implement password-based authentication by using TLS to set up a secure channel over which the password is sent, there are many arguments in favor of using PAKE protocols in conjunction with TLS [START_REF] Jarecki | OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks[END_REF]. Continued interest in PAKE is indicated by the fact that several PAKE protocols are currently under active consideration for standardization by the IETF [START_REF] Krawczyk | The OPAQUE asymmetric PAKE protocol[END_REF].

Defining security for PAKE protocols is made challenging by the fact that a password shared by the parties may have low entropy, and so can be guessed by an adversary with noticeable probability. This must somehow be accounted for in any security definition. Roughly speaking, the security guaranteed by a PAKE protocol is that an attacker who initiates Q online attacks-i.e., actively interferes in Q sessions of the protocol-can make at most Q password guesses (i.e., at most one per session in which it interferes) and can succeed in impersonating a party only if one of those guesses was correct. In particular, this means that offline attacks, in which an adversary merely eavesdrops on executions of the protocol, should not help the adversary in any way.

Two paradigms of PAKE security. In the cryptographic literature there are two leading paradigms for defining the above intuition. The first is the socalled "game-based" definition introduced by Bellare et al. [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF]. Here, a password is chosen from a distribution with min-entropy κ, and the security experiment considers an interaction of an adversary with multiple instances of the PAKE protocol using that password. A PAKE protocol is considered secure if no probabilistic polynomial-time (PPT) attacker can distinguish a real session key from a random session key with advantage better than Q•2 -κ plus a negligible quantity.

A second approach uses a "simulation-based" definition [START_REF] Boyko | Provably secure password-authenticated key exchange using Diffie-Hellman[END_REF][START_REF] Canetti | Universally composable password-based key exchange[END_REF]. The most popular choice here is to work in the universal composability (UC) framework [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF], and this is what we assume here. This approach works by first defining an appropriate ideal functionality for PAKE; a PAKE protocol is then considered secure if it realizes that functionality in the appropriate sense. Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF] pursued this approach, and defined a PAKE functionality that explicitly allows an adversary to make password guesses; a random session key is generated unless the adversary's password guess is correct. As argued by Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF], this approach has a number of advantages. A definition in the UC framework is better suited for handling general correlations between passwords, e.g., when a client uses unequal but related passwords with different servers, or when an honest party uses different but closely related passwords due to mistyping. It also ensures security under arbitrary protocol composition, which is useful for arguing security of protocols that use PAKE as a subroutine, e.g., for converting symmetric PAKE to asymmetric PAKE [START_REF] Gentry | A method for making password-based key exchange resilient to server compromise[END_REF][START_REF] Hwang | Round-reduced modular construction of asymmetric password-authenticated key exchange[END_REF] or strong asymmetric PAKE [START_REF] Jarecki | OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks[END_REF]. This is especially important in the context of PAKE standardization, because strong asymmetric PAKE protocols can strengthen the current practice of password-over-TLS authentication while achieving optimal security against server compromise.

Is there an inherent price for simulation-based security? Simulationbased security for PAKE is a desirable target. Unfortunately, the current state-ofthe-art [START_REF] Canetti | Universally composable password-based key exchange[END_REF][START_REF] Katz | Round-optimal password-based authenticated key exchange[END_REF][START_REF] Jutla | Dual-system simulation-soundness with applications to UC-PAKE and more[END_REF][START_REF] Bradley | Passwordauthenticated public-key encryption[END_REF] suggests that this notion is more difficult to satisfy than the game-based definition. In particular, the most efficient UC PAKE protocol [START_REF] Bradley | Passwordauthenticated public-key encryption[END_REF] is roughly a factor of two less efficient than the most efficient game-based PAKEs1 such as SPEKE [START_REF] Jablon | Extended password key exchange protocols immune to dictionary attacks[END_REF][START_REF] Mackenzie | On the security of the SPEKE password-authenticated key exchange protocol[END_REF][START_REF] Hao | The SPEKE protocol revisited[END_REF], SPAKE2 [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF], or TBPEKE [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF].

Perhaps surprisingly, we show here that this "gap" can be overcome; in particular, we show that the SPEKE, SPAKE2, and TBPEKE protocols-which were previously only known to be secure with respect to the game-based notion of security-can be shown to be universally composable (in the random-oracle model). The caveat is that we prove universal composability with respect to a relaxed version of the PAKE functionality originally considered by Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF]. At a high level, the main distinction is that the UC PAKE functionality of Canetti et al. requires an attacker conducting an online attack against a session to make its password guess before that session is completed, whereas the relaxed functionality we consider-which we call lazy-extraction PAKE (lePAKE)allows the attacker to delay its password guess until after the session completes. (However, the attacker is still limited to making a single password guess per actively attacked session.) On a technical level, this relaxed functionality is easier to realize because it allows the simulator to defer extraction of an attacker's password guess until a later point in the attacker's execution (see further discussion below). Nevertheless, the lazy-extraction PAKE functionality continues to capture the core properties expected from a PAKE protocol. In particular, as a sanity check on the proposed notion, we show that lePAKE plus key confirmation satisfies the game-based notion of PAKE with perfect forward secrecy (PFS) [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF][START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF][START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF].

Implications for PAKE standardization. Recently, the Crypto Forum Research Group (CFRG), an IRTF (Internet Research Task Force) research group focused on applications of cryptographic mechanisms, initiated a PAKE selection process with the goal of providing recommendations for password-based authenticated key establishment for the IETF. Originally, four candidates were under consideration by the CRFG in the symmetric PAKE category; the final decision was between SPAKE2 and CPace, and the latter was ultimately selected. Our results validate the security of SPAKE2 and the proof we provide for TBPEKE will be adapted to cover CPace and included in the full version [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF].

Technical Overview

The fundamental reason for an efficiency gap between known protocols achieving game-based PAKE and simulation-based PAKE is that the UC PAKE functionality, as defined by Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF] and used in all subsequent work, requires the adversary's password guesses to be (straight-line) extractable from the adversary's messages to the honest parties. Recall that for a PAKE to be UC secure there must exist an efficient simulator which simulates PAKE protocol instances given access to the ideal PAKE functionality, which in particular requires the simulator to specify a unique explicit password guess for each PAKE instance which the real-world adversary actively attacks. (The ideal PAKE functionality then allows the simulator, and hence the real-world adversary, to control the session key output by this instance if the provided password guess matched the password used by that PAKE instance, and otherwise the session key is random and thus secure.) The fact that the simulator must specify this explicit password before the attacked PAKE instance terminates, requires the simulator to online extract the password guess committed to in adversary's messages. Moreover, this extraction must be performed straight-line, because universal composibility prohibits rewinding the adversary.

Unfortunately, online extraction cannot be done for many efficient gamebased PAKE's listed above, because in these protocols each party sends a single protocol message which forms a perfectly hiding commitment to the password. Specifically, if g generates group of prime order p then in SPAKE2 each party sends a message of the form X = g z • P i pw where z ← R Z p , P 1 , P 2 are random group elements in the CRS, and i = 1 or 2 depending on the party's role. In TBPEKE, this message has the form X = (P 1 • P 2 H(pw ) ) z , and in SPEKE it is X = H(pw ) z where H is a hash onto the group. These commitments are binding under the discrete logarithm hardness assumption (the first two are variants of the Pedersen commitment [START_REF] Pedersen | Non-interactive and information-theoretic secure verifiable secret sharing[END_REF] and the third one requires the random-oracle model), and they are equivocable, i.e., the simulator can "cheat" on messages sent on behalf of the honest parties, but they are perfectly hiding and thus not extractable. These commitments can be replaced with extractable ones, but it is not clear how to do so without increasing protocol costs (or resorting to ideal ciphers over a group).

PAKE with post-execution input extraction. However, in all the above schemes the final session key is computed by hashing the protocol transcript and the Diffie-Hellman key established by this PAKE interaction, e.g. Z = g z1•z2 in SPAKE2 or Z = (H(pw )) z1•z2 in SPEKE. Since this final hash is modeled as a random oracle (RO), an adversary who learns any information on the session key must query this RO hash on the proper input. If the information in this hash query suffices for the simulator to identify the unique password to which this query corresponds, then a protocol message together with the final hash inputs do form an extractable commitment to the unique password guess the adversary makes on the attacked session.

However, the hash used in the final session key derivation is a local computation each party does in a "post-processing" stage which can be executed after the counterpart terminates the protocol. Therefore a simulator which extracts a password guess from the adversary's protocol message(s) and this local hash computation might extract it after the attacked session terminates. By the rules of the PAKE functionality of Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF], such extraction would happen too late, because the PAKE functionality allows the simulator to test a password guess against a session but does so only when this session is still active (and has not been attacked previously e.g. on a different password guess). Indeed, it would seem counter-intuitive to allow the ideal-world adversary, i.e., the simulator, to provide the unique effective password guess after the attacked session completes. Nevertheless, this is exactly how we propose to relax the UC PAKE functionality in order to accommodate protocols where input-extraction is possible, but succeeds only from the adversary's post-processing computation.

The relaxation we propose, the lazy-extraction PAKE, will require the idealworld adversary to "interrupt" a fresh session while it is active in order to then perform the post-execution password test (we will call such tests "late" password tests). This models the UC PAKE requirement that an adversary can use an honest PAKE session as a password-testing oracle only if it actively attacks that session, and in particular it still holds that passively observed sessions do not provide any avenue for an attack. (To keep the new elements of the lazy-extraction PAKE model clear we use separate terms, resp. RegisterTest and LateTestPwd, for this new type of online session interruption and for the late password test, see Section 2.) Moreover, even if the adversary chooses this "lazy-extraction attack" route, the functionality still allows for only a single password test on an actively attacked session. This requirement effectively commits a (computationally bounded) real-world adversary to a unique password guess on each actively attacked session, because an adversary who performs the local computation related to more than one password test would not be simulatable in the model where the ideal-world adversary can submit at most one such test to the lazy-extraction PAKE functionality.

Explicit authentication and perfect forward security. To test the proposed lazy-extraction UC PAKE notion we show two further things. First, we show that any lazy-extraction UC PAKE followed by a key confirmation round upgrades lazy-extraction UC PAKE to PAKE with explicit (mutual) authentication (PAKE-EA) [START_REF] Groce | A new framework for efficient password-based authenticated key exchange[END_REF], but it also realizes a stronger variant of lazy-extraction PAKE functionality which we call the relaxed UC PAKE. In the relaxed PAKE model, the adversary can still make a (single) late password test on an actively attacked session but such sessions are guaranteed to terminate with an abort. Hence, the attacker cannot use a late password test to compromise a session. Intuitively, if a lazy-extraction PAKE is followed by a key confirmation and the attacker delays its late password test until after the key confirmation is sent, then the key confirmation must fail and its counterpart will abort on such session. Hence, the "late password test" reveals if the tested passworded was correct but it cannot reveal a key of an active session.

Secondly, we show that any relaxed UC PAKE satisfies the game-based notion of PAKE with perfect forward secrecy (PFS) [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF][START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF][START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF]. (A similar test was done by Canetti et al. with regard to the original UC PAKE notion [START_REF] Canetti | Universally composable password-based key exchange[END_REF].) Intuitively, since the lazy-extraction attack avenue against a relaxed PAKE cannot be used to compromise keys of any active session, it follows that all active sessions, i.e., all sessions which terminate with a session key as opposed to an abort, are as secure in the relaxed UC PAKE model as they are in the original UC PAKE model of Canetti et al. In particular, they are secure against future password compromise.

Related and concurrent work. Jarecki et al. [START_REF] Jarecki | OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks[END_REF] recently introduced the relaxed UC PAKE model in the context of the asymmetric PAKE (aPAKE) functionality [START_REF] Gentry | A method for making password-based key exchange resilient to server compromise[END_REF], and showed that this relaxation is necessary to prove security of the OPAQUE protocol proposed in [START_REF] Jarecki | OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks[END_REF]. As discussed above, the lazy-extraction PAKE model goes further than the relaxed PAKE model, and this further relaxation appears to be necessary in order to model protocols like SPEKE, SPAKE2, and TBPEKE as universally composable PAKEs. (See Section 2 for the precise specifications of the lazy-extraction PAKE and the relaxed PAKE models.)

Hasse and Labrique [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] have recently argued that CPace [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] realizes a variant of the lazy-extraction UC PAKE functionality, but the variant of this notion they consider seems unsatisfactory, e.g. it appears not to imply security of passively observed sessions, and it appears to be not realizable as stated (see Section 2 for discussion). They also argue that adding a key-confirmation step suffices to convert such protocol into a standard UC PAKE, while we show that the result is still only a relaxed UC PAKE. 2In concurrent work, Shoup [START_REF] Shoup | Security analysis of spake2+[END_REF] analyzes the UC security of two variants of SPAKE2 in the symmetric (PAKE) and asymmetric (aPAKE) settings. Both variants include built-in key confirmation and the protocol flows are simplified so that only the initiator uses the password for blinding its first message. Shoup shows these protocols UC secure with respect to revised ideal functionalities for PAKE and aPAKE, under a slightly weaker assumption than the one required by our modular proof, namely strong Diffie-Hellman [START_REF] Abdalla | The oracle Diffie-Hellman assumptions and an analysis of DHIES[END_REF] instead of Gap CDH. (Strong DH is a variant of Gap CDH where the DDH oracle can be queried on triples whose first element is fixed.) The revised UC PAKE functionality considered in [START_REF] Shoup | Security analysis of spake2+[END_REF] appears equivalent to the relaxed UC PAKE functionality which we show is realized by SPAKE2 with key confirmation.

Publication Note

The work of Abdalla and Barbosa [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF], which provides a game-based security analysis of SPAKE2, has been merged with the current paper. However, since the focus of the present work is on the UC security analysis of practical PAKE schemes, we omit specific game-based security analyses of SPAKE2 here and refer the reader to [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF] for these analyses.

Paper Overview

In Section 2, we introduce the two relaxations of the UC PAKE functionality, namely the lazy-extraction UC PAKE and relaxed UC PAKE functionalities, respectively abbreviated as lePAKE and rPAKE, together with the extension of the latter to explicit (mutual) authentication. In Section 3, we show that SPAKE2 scheme of [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF] is a secure lePAKE under the Gap CDH assumption. In Section 4, we show that any lePAKE protocol followed by a key confirmation round is a secure rPAKE-EA, i.e., rPAKE with explicit authentication. In Section 5, we show that every rPAKE-EA protocol satisfies the game-based notion of PAKE with perfect forward secrecy, and that every lePAKE protocol by itself already satisfies weak forward secrecy. In Section 6, we also include the proof that TBPEKE [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF] is a secure lePAKE protocol under appropriate assumptions, and we explain that this proof extends to similar results regarding SPEKE [START_REF] Jablon | Extended password key exchange protocols immune to dictionary attacks[END_REF][START_REF] Mackenzie | On the security of the SPEKE password-authenticated key exchange protocol[END_REF][START_REF] Hao | The SPEKE protocol revisited[END_REF] and other variants of TBPEKE.

Relaxations of UC PAKE

In Fig. 1, we present the PAKE functionality as defined by Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF], and compare it with two relaxations that we refer to as relaxed PAKE (rPAKE) and lazy-extraction PAKE (lePAKE). We explain at a high level the differences between these various formulations. In the original PAKE functionality F PAKE , after a party initiates a session (but before the party generates a key) the attacker may try to guess the password used in that session by making a single TestPwd query. If the attacker's password guess is correct, the session is marked compromised; if not, the session is marked interrupted. When a session key is later generated for that session, the attacker is given the ability to choose the key if the session is marked compromised, but a random key is chosen otherwise. Importantly, the attacker is only allowed to make a password guess for a session before the key is generated and the session terminates.

In both the relaxed PAKE functionality F rPAKE and the lazy-extraction PAKE functionality F lePAKE , the attacker is given the ability to make a password guess for a session even after a session key is generated and that session has completed. Formally, this is allowed only if the attacker makes a RegisterTest query before the session key is generated; this indicates the attacker's intention to (possibly) make a password guess later, and models active interference with a real-world protocol execution. (Of course, the attacker also has the option of making a password guess before a key is generated as in the original F PAKE .) Having made a RegisterTest query for a session, the attacker may then make a LateTestPwd query to that session after the session key K is generated. F rPAKE and F lePAKE differ in what happens next:

First, in F rPAKE , the attacker is only told whether or not its password guess is correct, but learns nothing about K in either case. Secondly, in F lePAKE , the attacker is given K if its password guess is correct, and given a random key otherwise. 3It is easy to see that both F rPAKE and F lePAKE are relaxations of F PAKE , in the sense that any protocol realizing F PAKE also realizes F rPAKE and F lePAKE . Although, as defined, F lePAKE and F rPAKE are incomparable, the version of F lePAKE in which the attacker is additionally notified whether its password guess is correct (cf. Footnote 3) is a strict relaxation of F rPAKE .

Following the work of Groce and Katz [START_REF] Groce | A new framework for efficient password-based authenticated key exchange[END_REF], we also consider PAKE functionalities that incorporate explicit (mutual) authentication, which we refer to as PAKE-EA. 4 Intuitively, in a PAKE-EA protocol a party should abort if it did not establish a matching session key with its intended partner. As in the case of PAKE, the original PAKE-EA functionality introduced by Groce and

Session initiation

On (NewSession, sid , P, P , pw , role) from P, ignore this query if record sid , P, •, •, • already exists. Otherwise record sid , P, P , pw , role marked fresh and send (NewSession, sid , P, P , role) to A.

Active attack

-On (TestPwd, sid , P, pw * ) from A, if ∃ a fresh record sid , P, P , pw , • then:

• If pw * = pw then mark it compromised and return "correct guess";

• If pw * = pw then mark it interrupted and return "wrong guess". -On (RegisterTest, sid , P) from A, if ∃ a fresh record sid , P, P , •, • then mark it interrupted and flag it tested.

-On (LateTestPwd, sid , P, pw * ) from A, if ∃ a record sid , P, P , pw , •, K marked completed with flag tested then remove this flag and do:

• If pw * = pw then return K "correct guess" to A;

• If pw * = pw then return K $ ←R {0, 1} κ "wrong guess" to A.

Key generation

On (NewKey, sid , P, K * ) from A, if ∃ a record sid , P, P , pw , role not marked completed then do:

-If the record is compromised, or either P or P is corrupted, then set K := K * .

-If the record is fresh and ∃ a completed record sid , P , P, pw , role , K with role = role that was fresh when P output (sid , K ), then set K := K . -In all other cases pick K ←R {0, 1} κ . Finally, append K to record sid , P, P , pw , role , mark it completed, and output (sid , K) to P. Fig. 1. UC PAKE variants: The original PAKE functionality F PAKE of Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF] is the version with all gray text omitted. The relaxed PAKE functionality F rPAKE includes the gray text but omits the boxed portions; the lazy-extraction PAKE functionality F lePAKE includes the gray text but omits the dashed portions.

Session initiation

On (NewSession, sid , P, P , pw , role) from P, ignore this query if record sid , P, •, •, • already exists. Otherwise record sid , P, P , pw , role marked fresh and send (NewSession, sid , P, P , role) to A.

Active attack

-On (TestPwd, sid , P, pw * ) from A, if ∃ a fresh record sid , P, P , pw , • then:

• If pw * = pw then mark it compromised and return "correct guess";

• If pw * = pw then mark it interrupted and return "wrong guess". -On (RegisterTest, sid , P) from A, if ∃ a fresh record sid , P, P , •, • then mark it interrupted and flag it tested.

-On (LateTestPwd, sid , P, pw * ) from A, if ∃ a record sid , P, P , pw , •, K marked completed with flag tested then remove this flag and do:

• If pw * = pw then return "correct guess" to A.

• If pw * = pw then return "wrong guess" to A.

Key generation and explicit authentication

-On (GetReady, sid , P) from A, if ∃ a record sid , P, P , pw , role marked fresh then re-label it ready. -On (NewKey, sid , P, K * ) from A, if ∃ a record sid , P, P , pw , role not marked completed then do:

• If the record is compromised, or P or P is corrupted, or K * = ⊥ , then set K:=K * . • Else, if the record is fresh or ready, and ∃ a record sid , P , P, pw , role marked ready s.t. role = role then pick K ←R {0, 1} κ .

• Else, if the record is ready and ∃ a completed record sid , P , P, pw , role , K with role = role that was fresh when P output (sid , K ), then set K := K . • In all other cases, set K := ⊥ . Finally, append K to record sid , P, P , pw , role , mark it completed, and output (sid , K) to P. Fig. 2. The F rPAKE-EA functionality for relaxed PAKE-EA. The original PAKE-EA of Groce and Katz [START_REF] Groce | A new framework for efficient password-based authenticated key exchange[END_REF] corresponds to the version with gray text omitted. The boxed text highlights the differences from F rPAKE .

Katz required the attacker to make its password guess before the session key is generated, while we introduce a relaxed version of the PAKE-EA functionality, denoted F rPAKE-EA and shown in Fig. 2, that allows the attacker to delay its password guess until after the session has completed. 5 If the attacker's guess is correct, it is notified of that fact; our relaxation thus parallels that of F rPAKE . Note that such late password guess can only be performed on aborted sessions, since the attacker must send a RegisterTest query before the session completes, which marks the session interrupted, and by the rule of explicit authentication, an interrupted session must result in aborting.

Besides the intuitive appeal of our relaxed definitions, we justify these relaxations by showing that it is easy to realize F rPAKE-EA in the F lePAKE -hybrid world (Section 4), that any protocol realizing F rPAKE satisfies perfect forward secrecy (Section 5), and that any protocol realizing F lePAKE satisfies weak forward secrecy (Section 5.3).

Note on the relaxed PAKE functionality used in [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF]. A preliminary version of the lazy-extraction PAKE functionality, referred as "relaxed PAKE" therein, appeared in an early version of [START_REF] Jarecki | OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks[END_REF] and was adopted by [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] as a model for the CPace protocol. This version was imprecise in several respects: First, it does not require the adversary to explicitly attack an online session via a RegisterTest query before issuing a LateTestPwd query on a completed session. This appears too weak, e.g. because it allows an adversary to issue LateTestPwd queries even on passively observed sessions. On the other hand, it restricts the adversary from making a LateTestPwd query upon completion of the matching counterpart's session (with a matching sid but not necessarily a matching password), which appears too strong, because a man-in-the-middle attacker can make P complete with a random key or an abort, and this does not affect its capabilities regarding party P. Our lazy-extraction PAKE functionality makes this notion more precise, and in Section 6 we show that TBPEKE [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF] and SPEKE [START_REF] Jablon | Extended password key exchange protocols immune to dictionary attacks[END_REF] realize the lePAKE fuctionality under (Gap) CDH and/or SDH assumptions. Since CPace [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF][START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] is a close variant of SPEKE, these results can be extended to cover CPace as well. 63 Security of SPAKE2

We consider SPAKE2 as a motivating example for our work. SPAKE2 was proposed by Abdalla and Pointcheval [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF] and shown secure in the game-based PAKE model [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF] under the CDH assumption in the random-oracle model. SPAKE2 is, to the best of our knowledge, the most efficient PAKE protocol which does not assume ideal cipher over a group. Its costs are 2 fixed-base and 1 variable-base exponentiations per party, and it is round-minimal because it can be executed in a single simultaneous round of bi-directional communication.

We show that SPAKE2 realizes the lazy-extraction UC PAKE functionality under the Gap CDH assumption, and the result is tight in the sense that any environment which distinguishes between the real-world execution of SPAKE2 and the ideal-world interaction with a simulator and the lazy-extraction PAKE functionality, and does so in time T with advantage , implies an attack on Gap CDH which achieves roughly the same (T, ) advantage, where "roughly" means that both T and are modified by only additive factors. This UC security proof complements the result that SPAKE2 meets the game-based PFS definition [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF], which was not considered in [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF]. Interestingly, the game-based PFS result of [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF] is not tight: The proof relies on a special assumption introduced in [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF] for which a reduction to Gap CDH is known, but it is not a tight reduction. Still, since we do not know that lazy-extraction UC PAKE security implies PFS security by itself, this result is the only one we currently know for PFS security of (raw) SPAKE2. 7We recall the two-flow, simultaneous round SPAKE2 protocol of [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF] in Fig. 3, with some notational choices adjusted to the UC setting.

Public parameters: generator g and random elements M, N of group G of prime order p; hash function H : {0, 1} * → {0, 1} κ P on (NewSession, sid, P, P , pw , client): P on (NewSession, sid, P , P, pw , server):

x ←R Zp y ←R Zp X ← g x • M pw Y ← g y • N pw - X Y Ŷ ← Y /N pw X ← X/M pw K ← H(sid , P, P , X, Y, pw , Ŷ x ) K ← H(sid , P, P , X, Y, pw , Xy ) output K output K Fig. 3. SPAKE2 protocol of [7]
Theorem 1. SPAKE2 realizes the Lazy-Extraction PAKE functionality F lePAKE in the random-oracle model under the Gap-CDH assumption.

Gap CDH and Gap DL assumptions. Recall that the Computational Diffie-Hellman (CDH) assumption states that, given generator g and two random elements A = g a , and B = g b in a cyclic group of prime order, it is hard to find C = DH g (A, B) = g ab , while the Discrete Logarithm (DL) assumption states that it is hard to find a = DL g (A) given (g, A), for random A. In the gap version of either assumption, the respective problem must remain hard even if the adversary has access to a Decisional Diffie-Hellman oracle, which on any triple of group elements (A, B, C) returns 1 if C = DH g (A, B) and 0 otherwise. The Gap DL assumption follows via a trivial (and tight) reduction from the Gap CDH assumption, but we introduce it to highlight the fact that certain forms of adversarial behavior in SPAKE2 imply solving the harder problem of Gap DL.

Simulator for SPAKE2. The UC simulator SIM for SPAKE2, given in full in Fig. 4, acts as the ideal adversary, with access to the ideal functionality F lePAKE (shortened to F in the subsequent discussion). The simulator's goal is to emulate, except for at most negligible probability, the real-world interaction between the environment Z, a real-world adversary A, and honest parties running the SPAKE2 protocol. Technically, SIM must simulate messages that appear to come from the real players, respond appropriately to adversarial messages, and answer random-oracle queries consistently, and to do so with access to the F interface, but not the secret inputs, i.e., the passwords, of the honest players. We briefly describe how SIM simulates client P's interaction with an arbitrary environment Z and an adversary Adv. (The server case is similar since the protocol is symmetric.) SIM first embeds trapdoors into the CRS, i.e., it picks m, n ← R Z p and sets M = g m and N = g n . To simulate the protocol message X, SIM picks z ← R Z p and sets X = g z . Since X is also uniformly distributed in the real protocol, the environment cannot tell the difference. When A queries the random oracle H(sid , P, P , X, Y , pw, W ), SIM decides whether it corresponds to a valid password guess: SIM first computes the exponent x such that X = g x • M pw , using the CRS trapdoor m, and then checks if W = (Y /N pw ) x. If so, then SIM stores (Y , pw). If A later sends a protocol message Y aimed at P, then this is an online attack: when A makes the RO query, SIM picks a random string K as the output, and stores K together with (Y , pw ). Then, when A sends Y , SIM sends (TestPwd, sid, P, pw) to F, and if F replies "correct guess," then SIM sets P's key to K by sending (NewKey, sid , P, K) to F. (Otherwise, i.e., if F replies "wrong guess", SIM sends (NewKey, sid , P, 0 κ ) and F sets P's key to a random string.) On the other hand, if A makes an above query to H after sending Y to the client, then this is a postponed attack, so SIM sends (RegisterTest, sid, P) to F when A sends Y for which no such query has been made yet, and later sends (LateTestPwd, sid , P, pw ) to F when A makes the above query to H. If F then replies with a key K (which is either correct or random, depending on whether pw is correct or not), SIM "programs" H output as K. An adversary could distinguish this emulation from a real interaction by querying H on (sid , P, P , X, Y , pw i , W i ) tuples for W i = (Y /N pw i ) xi and xi = DL(X/M pwi ) for two different passwords pw i , but we show that this attack, as well as all others, can be reduced to Gap CDH.

Record keeping. For each party P and session sid , simulator SIM stores a state π sid P = (role, exp, C, S, X, Y, X * , Y * , pw, guesses, waiting) whose components are used as follows:

-Variable role ∈ {client, server} is the role of P in this session. (Note that in the protocol of Fig. 3 variable role is used only in the ordering of the identities in the hash H query.) -exp is the private exponent used in the network messages, x for C and y for S. In the first few games, it has the same meaning as in the protocol, but for SIM it is the discrete log of the simulated network message. waiting is a flag which is set to T for the session which has not received an adversarial message Z * , and F otherwise. This flag is used to ensure that only the first message an adversary sends to a session is processed, and all others are ignored.

Let Real Z,A,SPAKE2 be the probability of the event that environment Z with adversary A outputs 1 in the real world, and Ideal Z,SIM,SPAKE2 be the corresponding probability in the ideal world. The goal is to show that |Real Z,A,SPAKE2 -Ideal Z,SIM,SPAKE2 | is negligible. We use the well-known sequence-of-games proof strategy to show that we may move from the real game to the simulator in a manner indistinguishable to the environment, except for negligible probability. We begin with Game 0, the real game, and move through a series of steps, each of which we show to be indistinguishable from the previous, to the final simulator. Throughout the proof, Gi denotes the probability that Z outputs 1 while interacting with Game i.

Proof of Theorem 1.

Game 0. This is the real world, in which A interacts with real players, and may view, modify, and/or drop network messages.

Real Z,A,SPAKE2 = Pr [G0].
Game 1. (Simulate real world with trapdoors) We now simulate the behavior of the real players and the random oracle. The simulation is exactly as the real game, except for the inclusion of record keeping, and embedding of trapdoors in M and N , by setting M = g m and N = g n for known m and n. The embedding of trapdoors is not noticeable to the environment as M and N are still drawn from the same distribution as before, thus:

Pr [G1] = Pr [G0].
Game 2. (Random key if adversary is passive) If the adversary passes a simulated Z message sent to (sid , P) without modification, output a random key for P instead of the true random-oracle output. The environment notices this change only if A makes a hash query that would result in an inconsistency, namely H(sid , C, S, X , Y , pw , W = g xy ), where X = g x M pw and Y = g y N pw are the simulated messages. We check for such queries, and abort if any occur.

We may reduce this event to Gap-CDH as follows. Let q s be the maximum number of sessions invoked by the environment. Consider an adversary B 2 against Gap-CDH. On generalized CDH challenge 8

(A 1 = g a1 , • • • , A qs = g aq s , B 1 = g b1 , • • • , B qs = g bq s )
, the reduction indexes sessions (sid , P, P ), and embeds

X i = A i • M pw i , Y i = B i • N pw i
when generating the simulated messages for the ith session. The reduction can re-use the code of G2, except for the cases where it requires the secret exponents a i and b i : (1) to generate K ← H(sid , C, S, X, Y, pw , Ŷ ai {or Xbi }) and (2) to check for the "bad event" of an inconsistency in the hash response. To handle case (1), the reduction stores an additional value K for each session (sid , C, S) which is set randomly when either the reduction must handle case (1), or when A queries H(sid , C, S, X , Y , pw , W ) such that the password is correct and DDH(X , Y , W ) holds (checked via the DDH oracle): if either of these events happens again the same value of K is used. The check of case (2) can be done via the DDH oracle, i.e., by querying DDH(A i , B i , W ): if the bad event occurs, B 2 solves the CDH challenge with answer W . Thus:

|Pr [G2] -Pr [G1]| ≤ Adv GCDH B2 .
Game 3. (Random simulated messages) On (NewSession, sid , P, P , role), if this is the first NewSession for (sid , P), set Z ← g z for z ← R Z p , and send Z to A as a message from P to (P , sid ). Note that we may now compute the original exponents via:

x = m • π sid C .exp -m • pw and ŷ = n • π sid S .exp -n • pw .
This change is not observable to the environment, as it is merely a syntactic change in the calculation of the exponents:

Pr [G3] = Pr [G2].
Game 4. (Random keys if adversary does not correctly guess password) We now detect when an adversarial hash query corresponds to a password guess. We can detect this event by inspecting the X , Y , pw and W values provided to the hash oracle. Let us assume the adversary is guessing the client's password (the server case is symmetric). To make a password guess against the client, the adversary must set X = π sid C .X, i.e., use the simulated message sent by the client. The adversary can use any choice of Y , but to correspond with a specific password guess, the following must hold: W = (Y /N pw ) x (where x is the exponent such that π sid C .X = g xM pw ). In other words, W must be the value that would be used by a real client if Y were sent as the server's message. If such a password guess query is detected, we check if Y was previously sent as an adversarial message on behalf of the server: if so, and if the password guess is correct, we program the random oracle to match the previously sent key. If Y was not previously sent, we note the values Y , pw queried by the adversary and the random key K output by the RO. If Y is later sent as the adversarial message, and the password is correct, we output the stored key K. If the password is incorrect, we output a random key independent of the RO table. If at any point a second password guess (correct or incorrect) is detected for the same sid and party, we abort the game.

This change is noticeable to the environment only in the abort case, i.e, the case where the adversary makes two password guesses with a single (X , Y ) transcript, i.e.:

H(sid , P, P , X , Y , pw , Z) and H(sid , P, P , X , Y , pw , Z ), such that pw = pw , and CDH(g mx /M pw , g ny /N pw ) = Z and CDH(g mx /M pw , g ny /N pw ) = Z .

Call this event bad 4 . It can be split into two cases: 1) for one of the passwords pw * ∈ {pw , pw } it holds that X = M pw * or Y = N pw * , i.e., there is a collision between the guessed password pw * and the secret exponent x or y or 2) there is no such collision. Case 2, which we denote bad 1 4 , can be reduced to Gap-CDH, as shown in Lemma 1. Case 1 can be reduced to Gap-DL as follows: Adversary B 4.2 on Gap DL challenge A = g a , sets simulated messages as: X i = A•g ∆i,x and Y i = A • g ∆i,y , picking a fresh random ∆ i,x and ∆ i,y for each session (sid , P, P ). In the ith session (for every i), B 4.2 uses the DDH oracle to check for bad 4 . If true, B 4.2 further checks if Y = N pw * or X = M pw * for one of the passwords: in the former case this means that Y = N pw = A • g ∆i,y , so npw = a + ∆ i,y , and B 4.2 can output the DL solution is a = npw /∆ i,y , and the latter case is symmetric. We have that

|Pr [G4] -Pr [G3]| ≤ Adv GDL B4.1 + Adv GCDH B4.2 .
Game 5. (Use F lePAKE interface) In the final game, we modify the challenger so that it uses the RegisterTest, TestPwd and LateTestPwd interfaces to check passwords, and the NewKey interface to set keys. This is an internal change that is not noticeable to the environment, thus

Pr [G5] = Pr [G4].
Finally, we may solve for the desired CDH value:

g mn = (Z (x-pw ) • Z (pw -x) ) 1/(x-pw )(x-pw )(pw -pw )
This is possible as long as we are not dividing by zero, i.e., if pw = x and pw = x, which is explicitly excluded in the definition of event bad 1 4 (see Case 1 of G4 for handling of this case).

Remark on Gap CDH. The proof relies on the gap version of CDH, and it seems hard to prove security from the standard CDH assumption, because the Decision Diffie-Hellman oracle is used by CDH reductions to maintain consistency of answers to RO queries, and it is not clear how to ensure this consistency otherwise. This is also the case in the all the other PAKE protocols we consider in Section 6.

Adding Explicit Authentication

We will show that any protocol that securely realizes the lazy-extraction UC PAKE functionality F lePAKE , followed by a key confirmation round, is a secure realization of the relaxed UC PAKE-EA functionality F rPAKE-EA . (See Section 2 for the definition of these functionalities.) This protocol compiler construction is shown in Fig. 5.

P on (NewSession, sid , P, P , pw , client): P on (NewSession, sid , P , P, pw , server):

-(NewSession, sid , P, P , pw , client) (NewSession, sid , P , P, pw , server)

lePAKE prot. Π (sid , k) - (sid , k ) K = PRF k (1) K = PRF k (1) τC = PRF k (2) τS = PRF k (3) γC = PRF k (3) - τC τS γS = PRF k (2) if τS = γC: output (sid , K) if τC = γS : output (sid , K ) else: output (sid , ⊥)
else: output (sid , ⊥) Fig. 5. Compiler from lePAKE protocol Π to rPAKE-EA protocol Π .

Theorem 2. Protocol Π shown in Fig. 5 realizes the Relaxed PAKE-EA functionality F rPAKE-EA if Π realizes the Lazy-Extraction PAKE functionality F lePAKE and PRF is a secure PRF.

Fig. 6 shows the simulator used in the proof of Theorem 2. (For notational simplicity, we denote the functionality F rPAKE-EA as simply F.) For the formal proof of this theorem we refer to the full version of this paper [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF], but here we provide an informal overview.

The proof is essentially a case-by-case argument, where all possible scenarios are divided into several cases, according to whether A performs an online attack on party P's rPAKE session, and if so, whether it is an online attack or a postponed attack on P's lePAKE session. 9 Below we describe the cases, and how each case can be simulated:

Case 1 (online attack on lePAKE → online attack on rPAKE): A sends (TestPwd, sid , P, pw * ) to F lePAKE when P's lePAKE session is fresh.

In this case SIM passes (TestPwd, sid , P, pw * ) to F. If F replies with "correct guess", i.e., pw * = pw , then P's rPAKE session is compromised, so SIM can set its rPAKE output. Now on (NewKey, sid , k * ) from A, SIM can compute (K, τ, γ) from k = k * as the real-world session would, and send τ to A; on a tag τ * from A, SIM lets P output K if τ * = γ and ⊥ otherwise, matching the real-world execution.

On the other hand, if F replies with "wrong guess", i.e., pw * = pw , then P's rPAKE session is interrupted, hence P's rPAKE output is ⊥. SIM simply computes (K, τ, γ) from a random k and sends τ to A. This again matches the real-world execution with overwhelming probability: P's rPAKE output is ⊥ unless τ * = γ, which happens with negligible probability, and τ is computed in the exact same way.

Case 2 (postponed attack on lePAKE → online attack on rPAKE): A sends (RegisterTest, sid , P) when P's lePAKE session is fresh, followed by (NewKey, sid , P, k * ); and then sends (LateTestPwd, sid , P, pw * ) to F lePAKE (causing P's lePAKE session to complete) before sending a tag τ * to P. This is essentially the same as in Case 1, except that the order between the TestPwd (or LateTestPwd) queries and the NewKey query to F lePAKE is reversed. SIM can reverse the order of these two queries on the rPAKE level too, by sending a RegisterTest message to F first.

Case 3 (postponed attack on lePAKE → postponed attack on rPAKE): This is the complementary case of Case 2, i.e., A sends (RegisterTest, sid , P) when P's lePAKE session is fresh, followed by (NewKey, sid , P, ); and then a tag τ * to P before sending any (LateTestPwd, sid , P, pw * ) message to F lePAKE . (Eventually A may or may not send LateTestPwd.)

Again, in the real world P's rPAKE output is ⊥ unless τ * = γ, which happens with negligible probability, so SIM can simply let P output ⊥. However, if pw * = pw , A learns P's lePAKE output k (and thus can check if tag τ is the "correct" one, i.e., τ is derived from k using PRF). This can be simulated as follows: on NewKey from A, SIM computes (K, τ, γ) from a random k and sends τ to A; on τ * from A, SIM sends RegisterTest to F; on (LateTestPwd, sid , P, pw * ) from A, SIM passes this message to F, and if F replies with "correct guess", then SIM sends k to A, making τ the "correct" tag. (If F replies with "wrong guess", then SIM sends a fresh random key to A.)

Case 4 (no attack on lePAKE): A sends neither a (TestPwd, sid , P, ) nor a (RegisterTest, sid , P) query to F lePAKE when P's lePAKE session is fresh (thus P's lePAKE session remains fresh until it becomes completed).

In this case, A never learns P's lePAKE output k, so SIM can send a random tag τ to A. If A merely passes the tags between P and P , then SIM lets P complete its rPAKE session by sending (GetReady, sid , P) and then (NewKey, sid , P, 0 κ ) to F; if P and P 's passwords match, then P outputs a random K, otherwise P outputs ⊥. On the other hand, if A modifies the tag from P to P, then it is not the "correct" tag of P, so SIM lets P output ⊥.

Compiler from PAKE to PAKE with entity authentication. If we replace the lazy-extraction PAKE functionality with the (standard) PAKE, then the same compiler construction realizes the (standard) PAKE with explicit authentication functionality. In other words, by dropping the "laziness" of the underlying PAKE protocol, we get a compiler from PAKE to PAKE with explicit authentication. While technically not a corollary of Theorem 2, it is clear that the proof of Theorem 2 can be slightly modified to prove this conclusion: In that proof, the simulator SIM sends a password test (i.e., send a LateTestPwd message to F rPAKE-EA ) only if A does so (i.e., sends LateTestPwd message aimed at F lePAKE played by SIM); therefore, if both SIM and A are not allowed to do a late password test, the simulation will still succeed.

While it is well known that PAKE plus "key confirmation" yields PAKE with explicit authentication, to the best of our knowledge, there has been no proof of this fact in the UC setting.

SPAKE2 with key confirmation. An immediate corollary of Theorems 1 and 2 is that SPAKE2 with key confirmation realizes the relaxed UC PAKE-EA functionality F rPAKE-EA under the Gap-CDH assumption in the random-oracle model.

PAKE Relaxations and PFS

In this section we prove that any protocol that realizes the Relaxed PAKE functionality satisfies the standard game-based notion of security for PAKE protocols offering perfect forward secrecy (PFS). This is an important sanity check for the definition, as it shows that the extra power given to the ideal-world adversary by the late test feature does not weaken the security guarantee for PAKE sessions that are completed before passwords are corrupted. We show that a similar argument can be used to show that the weaker Lazy-Extraction PAKE definition implies a weak form of PFS, referred to as weak FS, where security in the presence of password leakage is only guaranteed with respect to passive attackers [START_REF] Katz | Forward secrecy in password-only key exchange protocols[END_REF][START_REF] Krawczyk | HMQV: A high-performance secure Diffie-Hellman protocol[END_REF].

Defining PFS

We recall the standard game-based notion of security for PAKE protocols and which follows from a series of works [START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF][START_REF] Abdalla | Password-based authenticated key exchange in the three-party setting[END_REF] that refined the security notion proposed by Bellare, Pointcheval and Rogaway in [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF]. Section 3 and [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF] include the full details.

The definition is based on an experiment in which a challenger emulates a scenario where a set of parties P 1 , . . . , P n , each running an arbitrary number of PAKE sessions, relies on a trusted setup procedure to establish pre-shared longterm (low-entropy) passwords for pairwise authentication. Passwords for each pair (P i , P j ) are sampled from a distribution over a dictionary D; we assume here the case where D is any set of cardinality greater than one, and each password is sampled independently and uniformly at random from this set. 10 A ppt adversary A is challenged to distinguish established session keys from truly random ones with an advantage that is better than password guessing.

The security experiment goes as follows. The challenger first samples passwords for all pairs of parties, generates any global public parameters (CRS) that the protocol may rely on and samples a secret bit b. The challenger manages a set of instances π j i , each corresponding to the state of session instance j at party P i , according to the protocol definition. The adversary is then executed with the CRS as input; it may interact with the following set of oracles, to which it may place multiple adaptive queries:

Execute: Given a pair of party identities (P i , P j ) this oracle animates an honest execution of a new PAKE session established between the two parties and returns the communications trace to the attacker. This gives rise to two new session instances π k i and π l j , which for correct protocols will have derived the same established session key. Send: Given a party identity P i , an instance j and a message m, this oracle processes m according to the state of instance π j i (or creates this state if the instance was not yet initialized) and returns any outgoing messages to the attacker. Corrupt: Given a pair of party identities (P i , P j ), this oracle returns the corresponding pre-shared password. Reveal: Given a party identity P i and an instance j, this oracle checks π j i and, if this session instance has completed as defined by the protocol, the output of the session (usually either a secret key or an abort symbol) is returned to the attacker. RoR: Given a party identity P i and an instance j, this oracle checks π j i and, if this session instance has completed as defined by the protocol and this session instance is fresh, the adversary is challenged on guessing bit b: if b = 0 then the derived key is given to the attacker; otherwise a new random key is returned. 11Eventually the adversary terminates and outputs a guess bit b . The definition of advantage excludes trivial attacks via the notion of session freshness used in the RoR oracle. Formal definitions are given in [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF], here we give an informal description. Two session instances are partnered if their views match with respect to the identity of the peer, exchanged messages and derived secret keys-the first two are usually interpreted as a session identifier. A session is fresh if: a) the instance completed; b) the instance was not queried to Ror or Reveal before; c) at least one of the following four conditions holds: i. the instance accepted during a query to Execute; ii. there exists more than one partner instance; iii. no partner instance exists and the associated password was not corrupted prior to completion; iv. a unique fresh partner instance exists (implies not revealed).

A PAKE protocol is secure if, for any ppt attacker interacting with the above experiment and placing at most q s queries to the Send oracle, we have that

| Pr[b = b] -1/2| ≤ q s /|D| + ,
where is a negligible term.

The original definition proposed by Bellare, Pointcheval and Rogaway [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF] allows for stronger corruption models-fixing the corrupt password maliciously and revealing the internal state of session instances-which we do not consider. We also do not deal with the asymmetry between client and server (also known as augmented PAKE).

Known results for UC PAKE. Canetti et al. [START_REF] Canetti | Universally composable password-based key exchange[END_REF] introduced the notion of UC-secure PAKE and proved that this definition implies game-based security of the protocol as defined in [START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF]. Our proof that Relaxed PAKE implies game-based PAKE with PFS follows along the same lines and relies on two auxiliary results from that original proof that we recover here; the first result concerns a generic mechanism for the handling of session identifiers called SID-enhancement and the second one is a general result for security against eavesdroppers.

Given a two-party protocol Π, its SID-enhancement Π is defined as the protocol that has the parties exchange nonces and then uses the concatenation of these nonces as SID. This transformation converts any protocol Π that assumes SIDs provided by an external environment as the means to define matching sessions, into another one that generates the SID on-the-fly as required by the syntax of the game-based security definition. Both the original proof and the one we give here show that the UC security of Π implies the game-based security of Π . Intuitively, an environment simulating the PFS-game above can wait until the SID for the enhanced protocol is defined before calling NewSession to initiate the session of the parties in the UC setting.

For security against eavesdroppers, Canetti et al. show that no successful ideal world adversary can place TestPwd queries on sessions for which the environment Z instructed the adversary to pass messages between the players unmodified (i.e., to only eavesdrop on the session). We give here the intuition on why this is the case and refer the interested reader to [START_REF] Canetti | Universally composable password-based key exchange[END_REF] for a detailed proof.

The crucial observation is that, for eavesdropped sessions, the ideal-world adversary generates all the trace and hence has no side information on the password; this means that for every environment Z for which the ideal-world attacker might place such a query, there exists an environment Z that can catch the simulator; Z operates as Z, but it uses a high-entropy password for the problematic session: in the real-world a session the two honest parties will endup with matching keys with probability 1-one assumes perfect correctness here for simplicity-whereas an ideal-world adversary placing a TestPwd can never match the same behaviour. Indeed, querying a wrong password to TestPwd leads to mismatching keys with overwhelming probability in the ideal world and the ideal-world adversary cannot guess the password correctly except with small probability.

This argument extends trivially to LateTestPw queries, as these must be preceded by a RegisterTest query prior to session completion that also leads to mismatching keys with overwhelming probability. Furthermore, the above reasoning also applies when the ideal-world adversary may have the extra power of simulating an ideal object, i.e., the UC-secure PAKE protocol is defined in an F-hybrid model. Indeed, whatever environment Z may have leaked to the ideal-world adversary via calls to F, there exists an environment Z that catches S as above.

Relaxed PAKE Implies PFS

Theorem 3. Let F be an ideal object such as a random oracle or an ideal cipher. If Π securely realizes F rPAKE without explicit authentication, in the (F CRS , F)hybrid model, then its SID-enhanced version Π is PFS-secure according to the game-based definition given above.

We refer to the full version of this paper [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF] for the proof of the above theorem, but this proof is quite similar to the proof of the corresponding theorem given in [START_REF] Canetti | Universally composable password-based key exchange[END_REF], which showed that the original notion of UC-secure PAKE implies gamebased security (with PFS) of a PAKE protocol.

Lazy-Extraction PAKE Implies Weak FS

The proof of the above theorem can be adapted to show that any protocol that realizes the Lazy-Extraction UC PAKE functionality is secure under a weak form of game-based security: the attacker is not allowed to corrupt the passwords of sessions against which it launches an active attack. This notion of game-based security for PAKE is sometimes called weak FS. The proof of the following theorem follows similar lines as the proof of Theorem 3, and we include it in the full version of this paper [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF].

Theorem 4. Let F be an ideal object such as a random oracle or an ideal cipher. If Π securely realizes F lePAKE without explicit authentication, in the (F CRS , F)hybrid model, then its SID-enhanced version Π is weak FS-secure.

Practical implications

Putting together the results in Section 3 and Section 4 we obtain positive results for rPAKE secure protocols in the Universal Composability framework, namely SPAKE2, TBPEKE, CPace and SPEKE, followed by a round of key confirmation (although we did not give a detailed proof for the latter). The result in this section shows that all such protocols are also PFS secure in the game-based setting. The caveat here is that this proof involves modifying the protocol to deal with session identifiers: The UC PAKE model requires a unique session identifier as an input of the protocol, while in practice agreeing on such identifier before the protocol starts can add extra communication rounds to the protocol. Nevertheless, a direct proof that SPAKE2 with key confirmation provides gamebased PFS with a tight reduction to Gap CDH in the random-oracle model can be found in [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF].

Security of TBPEKE, SPEKE, and their variants

In this section, we prove that the TBPEKE protocol proposed by Pointcheval and Wang [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF] also realizes the lazy-extraction PAKE functionality under the same assumptions which were used to prove its game-based security. Moreover, since TBPEKE is a representative example of a class of protocols which includes SPEKE [START_REF] Jablon | Extended password key exchange protocols immune to dictionary attacks[END_REF][START_REF] Mackenzie | On the security of the SPEKE password-authenticated key exchange protocol[END_REF][START_REF] Hao | The SPEKE protocol revisited[END_REF] and CPace [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF][START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF], the same likely holds for these other protocols as well, or for their close variants. For example, it is straightforward to adapt our security proof for TBPEKE to show that lazy-extraction UC PAKE functionality is realized under the same assumptions also by SPEKE [START_REF] Jablon | Extended password key exchange protocols immune to dictionary attacks[END_REF][START_REF] Mackenzie | On the security of the SPEKE password-authenticated key exchange protocol[END_REF][START_REF] Hao | The SPEKE protocol revisited[END_REF]. 12Due to its recent selection by the CFRG, we will analyze the specific case of CPace in the full version [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF]. 6 We now recall the two-flow, simultaneous round TBPEKE protocol [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF] in Fig. 7, with some notational choices adjusted to the UC setting. K ← H(sid , P, P , g pw , X, Y, X y ) output K output K Fig. 7. TBPEKE protocol of [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF], which uses an additional random oracle P for deriving the generator gpw .

For the security proof of TBPEKE we require the following computational assumptions [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF].

SDH and Gap SDH assumptions. The Simultaneous Diffie-Hellman (SDH) assumption states that, given three random elements X, g = X a , and h = X b in a cyclic group of prime order, it is hard to find Y = 1 and R, S that simultaneously satisfy R = CDH g (X, Y ) = Y 1/a and S = CDH h (X, Y ) = Y 1/b . In the gap version, the problem must remain hard even if the adversary has access to a Decisional Diffie-Hellman oracle. For the formal proof of Theorem 5, we refer to the full version of this paper [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF]. Here, we only present an informal overview of this proof and the simulator used in the proof, shown in Fig. 8.

The proof that TBPEKE is lazy-extraction UC PAKE secure is structurally similar to that of SPAKE2. In particular, the simulator adopts the same highlevel strategy for dealing with passive and active attacks, while simulating the random oracle that is used for key derivation by taking advantage of knowing the CRS. The random oracle P is trivially simulated, excluding collisions to avoid ambiguity between passwords. The sequence of games that justifies the simulation also follows the same pattern.

The only significant difference between the proofs for TBPEKE and SPAKE2 lies in the step where one must exclude the possibility that the adversary places two random-oracle queries for two different passwords that are consistent with the same protocol trace, which would prevent the simulator from maintaining consistency. In TBPEKE, this bad event corresponds to the case in which the adversary queries the hash oracle H on inputs (g pw 1 , X, Y , W 1 ) and (g pw 2 , X, Y , W 2 ) such that at least one of the values X and Y is simulated and (X, Y, W i ) is a valid DDH tuple with respect to the generator g pw i for i = 1, 2. In the SPAKE2 proof, the corresponding event can be reduced to Gap CDH. For TBPEKE, the reduction to Gap CDH does not work and the stronger Gap SDH assumption (given above) is needed.

The strategy for embedding a Gap SDH instance in the reduction is the same as that adopted in [START_REF] Pointcheval | VTBPEKE: Verifier-based two-basis password exponential key exchange[END_REF]. More precisely, the reduction guesses the two queries to the oracle P that correspond to the passwords that are involved in the bad event and programs the random oracle output for these passwords with two random values p 1 and p 2 from Z p . Then, given a Gap SDH challenge (A, G 1 , G 2 ), it sets V ← (G 1 /G 2 )

1/(p1-p2) and U ← G 1 /V p1 so that we have U • V pi = G i for i = 1, 2. Next, it embeds the value of A in the client and server messages X and Y (randomizing them appropriately) whenever it needs to simulate these values. Finally, if the bad event happens and the guesses for pw 1 and pw 2 are correct, then we know that (X, Y, W i ) is a valid DDH tuple with respect to the generator G i for i = 1, 2. If X = A α is the simulated value (the case in which Y is simulated is similar) and α is the randomization factor, then it follows that (Y, W

1/α 1 , W 1/α 2
) is a valid solution to the Gap-SDH problem.

  Public parameters: Random elements U, V of group G of prime order p; hash function H : {0, 1} * → {0, 1} κ ; hash function P : {0, 1} * → Zp P on (NewSession, sid, P, P , pw , client): P on (NewSession, sid, P , P, pw , server):gpw ← U • V P(pw ) g pw ← U • V P(pw ) x ←R Zp y ←R Zp X ← g x pw Y ← g y pw -X Y K ← H(sid , P, P , gpw , X, Y, Y x )

Theorem 5 .

 5 TBPEKE realizes the Lazy-Extraction PAKE functionality F lePAKE in the random-oracle model under the Gap-CDH and Gap Simultaneous Diffie-Hellman (Gap-SDH) assumptions.

  -C, S are the the party party identifiers for client and server respectively, X, Y are the simulated messages sent by resp. C and S (on sessions identified by sid ), and X * , Y * are the messages the adversary sends to resp. S and C. Simulator SIM stores messages X and Y * for the client (copying Y from the server if it exists), and symmetrically it stores Y and X * for the server (copying X from the client if it exists). Unknown values are set to ⊥.pw is a password used by party P on session sid . It is used only in intermediate games, while simulator SIM always sets it to ⊥. -guesses is a table mapping group elements Z * to pairs (pw, K

*

), representing potential password guesses and corresponding keys, which the simulator constructs from adversary's queries to oracle H of the form (sid , P, P , X, Z * , pw, •) if P plays the client role, and (sid , P , P, Y, Z * , pw, •) if P plays the server role. If the adversary sends Z * to party P, the simulator looks up the corresponding password pw, which it sends to F as a tested password.

Variants of EKE[START_REF] Bellovin | Encrypted key exchange: Password-based protocols secure against dictionary attacks[END_REF] shown to be universally composable[START_REF] Abdalla | Efficient two-party password-based key exchange protocols in the UC framework[END_REF][START_REF] Bradley | Passwordauthenticated public-key encryption[END_REF] may appear to be exceptions, but EKE requires an ideal cipher defined over a cryptographic group, and it is not clear how that can be realized efficiently.

In[START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] this is explicitly claimed not for CPace itself but for its asymmetric (aPAKE) version called AuCPace.

Note that here the attacker is not explicitly notified whether its password guess is correct. While it is arguably more natural to notify the attacker, we obtain a slightly stronger functionality by omitting this notification.

Although Canetti et al.[START_REF] Canetti | Universally composable password-based key exchange[END_REF] informally suggest a way of modeling explicit authentication in PAKE, the functionality they propose seems unacceptably weak in the sense that it does not require a party to abort even when an attacker successfully interferes with its partner's session.

While relaxing the Groce-Katz functionality, we also make some minor changes to their original: (1) we make the parties symmetric, and do not require the server to generate a session key first, and (2) we allow the adversary to force a party to abort by sending a (NewKey, sid , P, ⊥) message. (This second modification is required, and its omission appears to be an oversight ofGroce and Katz.)

In CPace[START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF], the key derivation hash includes only the session ID and the Diffie-Hellman key, while our proof of TBPEKE security assumes that it also includes party IDs, the password-dependent base, and the transcript. The final version of CPace selected by the CFRG has been updated to include all these elements except the password. In the full version[START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF], we will analyze the security of this version of CPace.

Note that the combined results of Sections 3 to 5 show that SPAKE2 followed by a key confirmation round is PFS secure, with tight security with respect to Gap CDH.

The generalized CDH problem is tightly equivalent to the CDH problem by random self-reducibility.

Note that each rPAKE session runs a lePAKE session as a subprotocol, and these two sessions should not be confused. Similarly, each party has a lePAKE output (which is always a string) and an rPAKE output (which is either a string derived from its lePAKE output or ⊥).

This assumption is standard for the corruption model captured by this game-based definition. If correlated passwords were allowed, then corrupting one password might reveal information that allows the attacker to trivially infer another one; preventing trivial attacks in this setting leads to a definition in the style of[START_REF] Bellare | Authenticated key exchange secure against dictionary attacks[END_REF], where the corruption of a password must invalidate RoR queries associated with all correlated passwords; this means the whole dictionary if no restrictions are imposed on the distribution. The finer-grained definition of password corruption we adopt here does not easily extend to the case of arbitrary correlations between passwords. See[START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF] for a discussion. The UC definition covers arbitrary password sampling distributions and the results we prove in this section should extend to any reasonable game-based definition that deals with more complex password distributions. This is clearly the case for the concrete distributions discussed in[START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF].

We use RoR (Real-or-Random) for this oracle rather than the standard Test oracle designation to avoid confusion with the test and late test requests that are included in the UC PAKE ideal functionality definitions.

For instance, in the case of SPEKE (in which g = G(pw )), one can adapt the proof for TBPEKE by simulating the random oracle G as U • V P(pw ) .

Acknowledgments. Michel Abdalla was supported in part by the ERC Project aSCEND (H2020 639554) and by the French ANR ALAMBIC Project (ANR-16-CE39-0006). Work of Manuel Barbosa was supported in part by the grant SFRH/BSAB/143018/2018 awarded by FCT, Portugal, and by the ERC Project aSCEND (H2020 639554). Stanis law Jarecki and Tatiana Bradley were supported by NSF SaTC award #1817143. Work of Jonathan Katz and Jiayu Xu was supported in part under financial assistance award 70NANB15H328 from the U.S. Department of Commerce, National Institute of Standards and Technology.

generate CRS M ← g m ; N ← g n for (m, n) ←R Zp return M, N on (NewSession, sid, P, P , role) from F if π sid P = ⊥: return ⊥ (X, Y ) ← (⊥, ⊥) if role = client :

(C, S) ← (P, P ) z ←R Zp ; X ← M z ; Z ← X if π sid P = ⊥ and π sid P .role = client: Y ← π sid P .Y ; π sid P .X ← X else if role = server :

(C, S) ← (P , P) z ←R Zp ; Y ← N z ; Z ← Y if π sid P = ⊥ and π sid P .role = server: X ← π sid P .X; π sid P .Y ← Y π sid P ← (role, z, C, S, X, Y, ⊥, ⊥, ⊥, ⊥, T) send Z from P to A on Z * from A as msg to (sid, P) if π sid P = ⊥ or π sid P .waiting = F: return ⊥ (role, •, C, S, X, Y, •, •, •, guesses, •) ← π sid

reply ← (TestPwd, sid, P, pw ) to F if reply = "correct": K ← K * else: send (RegisterTest, sid, P) to F end: π sid P .waiting ← F send (NewKey, sid, P, In addition, this simulator perfectly mimics the ideal world except for the cases where it aborts, which we have already shown to happen with negligible probability, so:

Thus the distinguishing advantage of Z between the real world and the ideal world is:

which is negligible if Gap-CDH is hard.

Lemma 1. For every attacker A, there exists an attacker B 4.1 (whose running time is linear in the running time of A) such that:

Proof. Consider an attacker B 4.1 against GCDH. It receives a challenge (M = g m , N = g n ) and wants to find CDH(M, N ) = g mn . The attacker emulates G4, except for setting the CRS values as M, N from the challenge instead of randomly. It uses the DDH oracle to carry out the three checks in the if/else if/else if structure of the hash response, and for detecting the bad event.

In particular, it detects the bad event bad 1 4 when it sees two hash queries (sid , X , Y , pw , Z) and (sid , X , Y , pw , Z ) such that pw = pw , and both of the following hold, where either x or y is known (i.e, chosen by the attacker as the exponent for a simulated message):

The attacker can then solve for the CDH response, g nm , as follows. First, write Z = g z ; Z = g z for unknown z, z ∈ Z p . Considering only the exponents in Eqs. ( 1) and (2), we have that:

Assume that the attacker knows the exponent x (the other case is symmetric). Scaling Eqs. ( 3) and (4) by resp. (x -pw ) and (x -pw ), gives:

Subtracting Eq. ( 6) from Eq. ( 5) allows us to remove the unknown y term:

On (NewSession, sid , P, P , role) from F If there is no record sid , P, . . . then: Send (NewSession, sid , P, P , role) to A and store sid , P, P , role marked fresh. On (TestPwd, sid , P, pw * ) from A If there is a fresh record sid , P, . . . then:

Send (TestPwd, sid , P, pw * ) to F; If F replies "correct guess" then pass it to A and mark this record compromised.

If F replies "wrong guess" then pass it to A and mark this record interrupted. On (RegisterTest, sid , P) from A If there is a fresh record sid , P, . . . then:

Mark this record interrupted and flag it tested. On (NewKey, sid , P, k * ) from A If there is a record sid , P, P , role not completed then:

Define k as follows: If this record is compromised, or P or P is corrupted, then set k := k * . Else if this record is interrupted (tested or not), then set k ←R {0, 1} Mark record sid , P, P , role "completed with key k and tag γ"; Send τ to A as the authenticator from P to P . On delivery of an authenticator from A If record sid , P, P , role is marked "completed with key k and tag γ", and A sends a purported authenticator, denoted τ * , to protocol instance (sid , P) then:

If sid , P, P , role is flagged tested: Send (RegisterTest, sid , P) to F. If k = ⊥ then:

If τ * = γ then send (NewKey, sid , P, PRF k (1)) to F. If τ * = γ then send (NewKey, sid , P, ⊥) to F. If k = ⊥ (i.e., the record was fresh right before it became completed) then:

If there is a completed record sid , P , P, role for role = role, which was marked fresh right before it became completed, and which sent out authenticator τ s.t. τ * = τ , then send (NewKey, sid , P, 0 κ ) to F. Else send (NewKey, sid , P, ⊥) to F. On (LateTestPwd, sid , P, pw * ) from A If there is a record sid , P, . . . marked "completed with key k", and flagged tested:

Remove the tested flag from this record; If A did not send an authenticator to protocol instance (sid , P) then send (TestPwd, sid , P, pw * ) to F; Else send (LateTestPwd, sid , P, pw * ) to F; If F replies "correct guess" then send k to A. If F replies "wrong guess" then send k $ ←R {0, 1} κ to A. Fig. 6. Simulation for relaxed PAKE-EA protocol in Figure 5.