Michel Abdalla
email: michel.abdalla@gmail.com

Manuel Barbosa

Jonathan Katz
email: jkatz2@gmail.com

Julian Loss
email: lossjulian@gmail.com

Jiayu Xu
email: jiayux@uci.edu

Algebraic Adversaries in the Universal Composability Framework

The algebraic-group model (AGM), which lies between the generic group model and the standard model of computation, provides a means by which to analyze the security of cryptosystems against so-called algebraic adversaries. We formalize the AGM within the framework of universal composability, providing formal definitions for this setting and proving an appropriate composition theorem. This extends the applicability of the AGM to more-complex protocols, and lays the foundations for analyzing algebraic adversaries in a composable fashion. Our results also clarify the meaning of composing proofs in the AGM with other proofs and they highlight a natural form of independence between idealized groups that seems inherent to the AGM and has not been made formal before-these insights also apply to the composition of game-based proofs in the AGM. We show the utility of our model by proving several important protocols universally composable for algebraic adversaries, specifically:

(1) the Chou-Orlandi protocol for oblivious transfer, and (2) the SPAKE2 and CPace protocols for password-based authenticated key exchange.

1 Introduction . . . . .

Introduction

Security proofs are often carried out in idealized models that seek to capture certain classes of adversarial behavior. Examples include the random-oracle model [START_REF] Bellare | Random oracles are practical: A paradigm for designing efficient protocols[END_REF], in which the attacker is assumed to treat a hash function as an ideal random function; the ideal-cipher model, in which the attacker is assumed to treat a block cipher as an ideal keyed permutation; and the generic-group model (GGM) [START_REF] Nechaev | Complexity of a determinate algorithm for the discrete logarithm[END_REF][START_REF] Shoup | Lower bounds for discrete logarithms and related problems[END_REF], where the attacker is assumed to treat group elements as abstract identifiers and group operations as black-box operations on those identifiers.

Cryptographers continually seek to refine these models, making them more expressive so they capture larger classes of algorithms and thus come closer to modeling adversaries performing arbitrary computation. With this motivation in mind, Fuchsbauer et al. [START_REF] Fuchsbauer | The algebraic group model and its applications[END_REF] (based on ideas of Abdalla et al. [START_REF] Abdalla | Security of the J-PAKE password-authenticated key exchange protocol[END_REF]) proposed the algebraic-group model (AGM) as a more expressive version of the GGM. Roughly, the AGM considers algebraic adversaries that compute group elements via a sequence of "generic" group operations, but which-in contrast to the GGM-are allowed to utilize the actual bitstrings representing group elements in the course of their computation. This model is strictly stronger than the GGM; for example, index-calculus algorithms that apply to certain classes of groups are algebraic and hence allowed in the AGM, even though they are ruled out in the GGM by known lower bounds on the hardness of the discrete-logarithm problem in that model. The AGM has been used to show equivalence of various number-theoretic assumptions [START_REF] Auerbach | Everybody's a target: Scalability in public-key encryption[END_REF][START_REF] Bauer | A classification of computational assumptions in the algebraic group model[END_REF][START_REF] Fuchsbauer | The algebraic group model and its applications[END_REF] and to prove security of SNARKs [START_REF] Chiesa | Marlin: Preprocessing zkSNARKs with universal and updatable SRS[END_REF][START_REF] Fuchsbauer | The algebraic group model and its applications[END_REF][START_REF] Maller | Sonic: Zero-knowledge SNARKs from linear-size universal and updatable structured reference strings[END_REF] and blind signatures [START_REF] Fuchsbauer | Blind schnorr signatures and signed ElGamal encryption in the algebraic group model[END_REF]. An extension called the strong AGM has recently been used to prove hardness of the repeated squaring assumption underlying timed commitments and related primitives [START_REF] Katz | On the security of time-lock puzzles and timed commitments[END_REF].

Notably, none of the aforementioned results provide any guarantees of security under composition with other protocols (whether proven secure in the AGM or not). Here, we lay the foundations for a composable treatment of algebraic adversaries by formalizing the AGM within the framework of universal composability (UC) [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF] and proving a corresponding composition theorem. This involves not only formalizing a number of subtle issues related to the AGM itself (which may be of independent interest for subsequent work in the AGM), but also making a number of careful design decisions in defining what algebraic adversaries mean in the UC framework, in part to ensure that a suitable composition theorem holds. We discuss this in more detail in the following section.

We demonstrate the utility of our model by proving several important protocols universally composable for algebraic adversaries. Specifically, we prove security of (1) the Chou-Orlandi protocol for oblivious transfer [START_REF] Chou | The simplest protocol for oblivious transfer[END_REF], and (2) the SPAKE2 and CPace protocols for password-based authenticated key exchange [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF][START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] in our model. We describe these results further in Section 1.2.

Defining the AGM Within the UC Framework

We first define some notation and terminology related to the AGM that suffices to understand the discussion that follows. (Our treatment here is deliberately informal, and we refer the reader to Section 2 for technical details.) Fix a group G. An algebraic representation of h ∈ G with respect to a list of elements g 1 , . . . , g n ∈ G is a tuple (x 1 , . . . , x n ) ∈ Z n with h = n i=1 g xi i . Roughly speaking, the AGM considers adversaries that are algebraic (with respect to G), meaning that if an adversary A outputs a group element h ∈ G, then A must also output an algebraic representation of h with respect to the set of group elements (which we call a base) that A has been given as input thus far.

We generalize the AGM to the standard UC framework by restricting our attention to algebraic attackers.1 While this is a natural idea, it involves dealing with a number of subtle technical issues. First of all, to make this notion meaningful it is not sufficient to restrict the adversary to be algebraic; rather, we require the environment to be algebraic as well. Moreover, in order for composition to possibly hold, we must also require the simulator used in proving security to be algebraic. That is, in the UC-AGM a protocol π securely realizes a functionality F if, for any efficient algebraic adversary A, there is an efficient algebraic simulator S such that no efficient algebraic environment can distinguish the execution of A with π from the execution of S with F. Under this definition, we can indeed prove that a UC-style composition theorem holds in the UC-AGM.

Our definition of an algebraic algorithm makes a distinction between adversarial entities (real and ideal world adversaries and environments) and non-adversarial entities (uncorrupted protocol participants and ideal functionalities). In the real world, we require the adversary to behave algebraically when it delivers group elements to uncorrupted participants and to ideal functionalities (when the proof is carried out in a hybrid real-world); moreover, we also require the environment to behave algebraically when it delivers group elements to the adversary, but not the converse. Algebraic behavior is defined within the context of a UC AGM proof by specifying what set of group elements occurring during the protocol execution in the real-world must be used by the environment and by the adversary as a base for the provided group element representations. When this is the empty set, we recover the standard UC framework. The natural definition for this set is to include in it all the group elements that are produced by non-adversarial entities.

We show this pictorially in Figure 1, where the blue arrows denote that all group elements that are delivered must be accompanied by an algebraic decomposition with respect to base B ρ , which are the group elements produced by the machines within the boundary of ρ. Note that, in the figure, ρ is specified in a hybrid world that includes a functionality F, which is within that boundary. The ideal world restrictions are equivalent, replacing A with S and ρ with the ideal-world protocol φ that is realized by ρ.

Formally, the quantification of the UC-emulation notion is subtle. As in UC, we require for all adversaries A, the existence of a simulator S, such that for all enviroments E the real and ideal worlds are indistinguishable. However, the simulator is only required to work if the pair (E, A) satisfies the algebraic restrictions specified in the real world. Intuitively, the extra power of the simulator comes from the fact that E is bound to behave algebraically when interacting with A and, furthermore, that A will also behave algebraically if the simulator runs it internally. A caveat is that the simulator must also ensure that (E, S) satisfy the algebraic restrictions in the ideal world. However, in the most common case when the simulator is interacting with an ideal functionality, if this interaction does not involve group elements, then the algebraic requirement is not a restriction on the simulation strategy (this is the case in all our proofs for concrete protocols).

The UC AGM composition theorem then states, as expected, that ρ π ∼ ρ F if π ∼ F. We show this scenario in Figure 2. Again the quantification is subtle. The composition theorem guarantees only hold if we restrict our quantification to match the emulation guarantee provided by π: i.e., we have that ρ π ∼ ρ F with respect to pairs (E, A) that adhere to the base B π when interacting with machines in π. Note that this means, in particular, that the attacker cannot use group elements produced in ρ when attacking π, unless it is able to provide a representation according to B π .

The companion UC AGM transitivity theory further highlights a natural notion of independence between UC AGM proofs. Suppose that ρ F is known to UC AGM emulate some functionality G. Transitivity intuitively implies that ρ π ∼ G if ρ π ∼ ρ F . We show that this is the case also in the UC AGM setting, if we restrict the quantification over (E, A) to those attackers that independently meet the AGM restrictions imposed by the proofs of both π and ρ. This means providing algebraic representations to parties executing π with respect to a base B π defined in the proof of π and, similarly, respecting the algebraic base B ρ when interacting with parties executing ρ. This restriction means that AGM UC composition works as expected for protocols that operate on groups that can be assumed to be independent.

In Section 2.3 we give full technical details and also show that proofs in the UC AGM naturally compose with proofs in the plain UC model; as expected, the composed protocols can only be shown to be secure in the UC AGM setting. We also show that the standard approach of writing UC proofs w.r.t. a dummy adversary still applies in the UC AGM setting.

Discussion. Our theorems show that one should be very careful when composing proofs in the AGM, and not only in the UC setting. For example, when composing game-based reductions carried out in the AGM, the same issues arise. Intuitively, composition can only be guaranteed when the AGM assumptions do not interact badly with each-other, i.e., interacting with one protocol does not allow an attacker to override the extractability assumption that is being captured by the AGM in the proof of another protocol. In practice this seems to imply excluding attackers that take group elements from one protocol and use them to attack another protocol (unless of course the algebraic construction of those elements can be explained with respect to the set of bases defined by the target protocol alone).

Interestingly, in recent independent work Kerber, Kiayias and Kohlweiss [START_REF] Kerber | Composition with knowledge assumptions[END_REF] encouter a manifestation of the same problem in the constructive cryptography framework. In this work, the authors propose a general notion of proofs w.r.t. knowledge assumptions, which generalizes the AGM: adversaries provide the relevant extractable information when interacting with the protocol. Their goal is to study the composition of protocols that rely on different knowledge assumptions. It is beyond the scope of this paper to make a detailed comparison, since the approaches rely on different compositional frameworks and have different goals, but it is clear that the same restrictions must be imposed in the composition theorem to enable a proof; quoting from the paper: "Care must be taken that knowledge stemming from one knowledge assumption does not give an advantage in another. . . we conjecture that multiple instances with the AGM with independently sampled groups are sufficiently independent."

To conclude, we do not see the restrictions in the UC AGM composition theorems as a limitation of our work, but rather as a limitation inherent to proofs in idealized models-for example, it is easy to establish a parallel with the random oracle model in the UC setting, where the need for independent RO instances is well known [START_REF] Canetti | Practical UC security with a global random oracle[END_REF]. On the contrary, we believe that an important contribution of our work is to clarify what this limitation means for proofs in the AGM. To overcome these limitations, and similarly to proofs in the random oracle model, one can prove multiple protocol executions secure simultaneously. At the very least, it is important to ensure that AGM UC proofs are carried out with respect to multi-session ideal functionalities, so that multiple executions of the same protocol can be guaranteed to compose securely. We adopt this approach in our proofs. Another option is to strengthen the proofs of each protocol to consider a global/shared source of bases along with a more powerful composition theorem, similarly to UC with global setup [START_REF] Canetti | Universally composable security with global setup[END_REF]. We leave exploring this option as an interesting and important direction for future work.

Proofs of Security in the UC-AGM

In addition to defining the UC-AGM framework, we also show that several important protocols from the literature-which were previously lacking full proofs of security in the UC framework-can be proven secure in our model.

The Chou-Orlandi protocol. Chou and Orlandi [START_REF] Chou | The simplest protocol for oblivious transfer[END_REF] proposed a simple and elegant protocol for oblivious transfer and claimed that it was universally composable (with adaptive corruptions) under a suitable assumption in the random oracle model. Unfortunately, subsequent works [START_REF] Byali | Fast and universally-composable oblivious transfer and commitment scheme with adaptive security[END_REF][START_REF] Genç | The simplest protocol for oblivious transfer" revisited[END_REF][START_REF] Hauck | Efficient and universally composable protocols for oblivious transfer from the CDH assumption[END_REF] uncovered several problems with their proof. While these subsequent works also showed how to address some of these issues, and/or presented modified protocols that could be proven secure, there seems to be no way of proving the original Chou-Orlandi protocol universally composable, even in the random oracle model.

We show that the original Chou-Orlandi protocol can be proven secure in the UC-AGM, based on the discrete-logarithm assumption in the random oracle model. We refer to Section 3 for a high-level overview of the proof and further details.

The SPAKE2 and CPace protocols. SPAKE2 [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF] and CPace [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF] have attracted a lot of interest recently due to their consideration for standardization by the IETF. The selection process explicitly considered whether these protocols were universally composable, which turned out to be a surprisingly difficult question to answer. 2Abdalla et al. [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF] recently proved that these protocols are universally composable with respect to a relaxed version of the standard functionality for password-based authenticated key exchange (PAKE) that, roughly speaking, allows the adversary to delay its password guess for a session until an arbitrary time after that session ends. The full implications of relying on that relaxed functionality are unclear; in particular, although Abdalla et al. [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF] showed that adding a key-confirmation step lifts a UC PAKE protocol to one that provides explicit entity authentication, we do not know if this is the case when we start from a PAKE protocol that only realizes the relaxed PAKE functionality.

In this work, we improve upon these results by showing that both SPAKE2 and CPace are universally composable with respect to the original PAKE functionality [START_REF] Canetti | Universally composable password-based key exchange[END_REF] when we restrict our attention to algebraic adversaries. Interestingly, our proofs are significantly simpler than those of Abdalla et al. [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF], since the simulator in our case can leverage the fact that the adversary is algebraic to directly extract password guesses, rather than performing an indirect extraction using the random oracle.

In addition, we also demonstrate that an important variant of SPAKE2, known as SPAKE1, is secure in the UC-AGM. SPAKE1, in contrast to SPAKE2, does not include the password as input to the final keyderivation function, and thus may be advantageous relative to SPAKE2 with regard to side-channel attacks targeting the key-derivation step. Prior to this work, SPAKE1 was not known to satisfy the standard notions of security for game-based and UC PAKE. In particular, it was not known to guarantee even the weaker notion of forward secrecy, in which the attacker can only learn passwords for sessions in which it played the role of a passive eavesdropper.

Related Work

We are not aware of any prior work modeling algebraic adversaries in the UC framework, however a few works have considered generic groups and other idealized models in that setting. Larangeira and Tanaka [START_REF] Larangeira | Programmability in the generic ring and group models[END_REF] analyze universally composable non-committing encryption schemes in the GGM and the generic-ring model (GRM). However, they leave the modeling of the GGM/GRM in the UC framework informal, and in particular do not prove that composition holds in their setting. Bradley et al. [START_REF] Bradley | Strong asymmetric PAKE based on trapdoor CKEM[END_REF] prove security of a strong asymmetric PAKE protocol against a generic-group adversary in the UC framework, but their treatment is also informal; in particular, their protocol is split into an "offline part" and an "online part," with the GGM used only in the former, and it is unclear how these two parts are defined for general protocols or what the implications are for composition. Naor et al. [START_REF] Naor | CHIP and CRISP: Compromise resilient identity-based symmetric PAKEs[END_REF] model generic-group adversaries in the UC framework by introducing a generic-group functionality F GGM in a way similar in spirit to the approach involving the F AGM functionality described earlier that we ultimately rejected. A similar approach was followed in [START_REF] Baum | Tardis: A foundation of time-lock puzzles in uc[END_REF] for the analysis of time-lock puzzles in the UC setting.

Overview of the Paper

Section 2 introduces the UC-AGM model. The treatment is quite low level to ensure the appropriate level of formalization and Appendix B.1 reviews the UC framework for this reason.Section 3 then presents a proof of the Chou-Orlandi protocol in the UC-AGM. Next, Section 4 proves security of SPAKE1, SPAKE2, and CPace in the new model. Finally, Appendices B to D provide detailed proofs for theorems in Sections 2 to 4.

Defining Algebraic Adversaries in the UC Framework

In this section, we introduce the UC-AGM framework that incorporates algebraic adversaries into the UC framework. We provide a brief overview of the UC framework [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF] in Section 2.1; for a more detailed description, see Appendix B.1 . In Section 2.2 we formally define algebraic adversaries and introduce the notation of AGM-emulation that underlies the UC-AGM. We also show there that, analogous to the UC framework, it suffices to consider "algebraically dummy" adversaries when proving AGM-emulation. We prove a composition theorem for the UC-AGM in Section 2.3.

For simplicity, our treatment of the UC-AGM is based on the so-called simplified UC framework [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]Section 2] where the number of parties, their identities, program code, and connectivity are all fixed in advance. In Appendix B.2 we explain how the UC-AGM can be extended to the full UC framework.

Overview of the UC Framework

A protocol consists of a number of machines (or parties) with unique identities, each of which represents some computational entity. Protocol machines communicate with each other via messages labeled input or subroutine-output. In an execution of the protocol, two additional machines (whose identities are distinct from any protocol machines) are added: the environment E and the adversary A. (Below we assume that E has identity 0 and A has identity 1.) The environment E can send input messages to A and a subset of the protocol machines (called main machines), and protocol machines can send subroutine-output messages to E; the adversary A can send backdoor messages to E and all protocol machines, and receive backdoor messages from all protocol machines.

The notion of UC emulation involves two protocols, π and φ. We say that π emulates φ if for any efficient adversary A in an execution of π, there is an efficient adversary (called the simulator ) S in an execution of φ that "simulates" the environment's view, in the sense that no efficient environment can distinguish an execution of π with A from an execution of φ with S. A particularly important example of UC emulation is realizing an ideal functionality, in which the emulated protocol ideal F consists of an incorruptible ideal functionality F, and the main machines are dummy parties that simply pass messages between the ideal functionality and the environment.

UC Emulation in the Algebraic Group Model

In this work we put forth a notion of UC emulation (called AGM-emulation) in which the adversary is restricted to be algebraic. To this end, we first introduce the concept of algebraic adversaries [START_REF] Fuchsbauer | The algebraic group model and its applications[END_REF]. At a high level, an algebraic adversary has an additional auxiliary tape on which it writes the representation of any group element it outputs on (some of) its other tapes. 3 We assume for simplicity that the group G = (G, g, p) under consideration is cyclic with known order p, though neither of these assumptions is essential. Definition 1. Suppose an execution of protocol π involves protocol machines sending elements in group G = (G, g, p) (henceforce "protocol π involves group G"). 4 A pair of environment E and adversary A (in π's execution) is (G, π)-algebraic if it satisfies the following:

(1) A has a special output tape called the algebraic tape;

(2) Whenever A sends (backdoor, m) to some protocol machine, where m contains some X ∈ G, then either (1) A also writes an algebraic representation of X on its algebraic tape, or (2) A has previously received such representation from E; where the algebraic representation of X is a list Λ = [(X 1 , λ 1 ), . . . , (X k , λ k )] (where X 1 , . . . , X k ∈ G and λ 1 , . . . , λ k ∈ Z p ) such that X = X λ1 1 • • • X λ k k , and X 1 , . . . , X k is the ordered list of group elements in messages E and/or A has received up to that point in the execution of π.

We stress that it is necessary to separate the algebraic tape from the other tapes of A so that, for example, the message m itself does not contain an algebraic representation of X. When clear from the context, we will drop G and π, and simply say that the environment/adversary is "algebraic."

We note that when considering static corruptions, the adversary runs the corrupt parties internally and hence messages produced by corrupt parties are subject to the restrictions above. The model for adaptive corruptions is the obvious one. Non-corrupt parties compute group elements honestly. So, if no secure erasure is assumed, the representations of any group elements computed by non-corrupt parties are part of their state when they are corrupted (and are given to the adversary). If we assume secure erasure, then any such state will not be available, and so any group elements that are part of a non-corrupt party's state will not have their representations available; in this case they must be added to the adversary's basis.

AGM emulation. We could now consider standard UC emulation restricted to algebraic adversaries and environments. However, looking ahead, in order for composition to hold we will want the simulator to be algebraic as well.

Definition 2. Suppose protocols π and φ involve the same group G. We say that π G-AGM emulates φ if the following holds: for any efficient adversary A, there is an efficient adversary S (called the simulator) such that: for any efficient E such that (E, A) are (G, π)-algebraic, we have that (E, S) are (G, φ)-algebraic, and exec φ,S,E ≈ exec π,A,E , where exec π,A,E denotes environment E's view in π's execution with adversary A.

Above, we write ≈ to denote generic computational indistinguishability. This may refer to either asymptotic indistinguishability, in which case a security parameter is introduced as well, or concrete indistinguishability, in which case we write ≈ to denote that the distinguishing advantage is bounded by . Definition 3. Protocol π G-AGM realizes ideal functionality F if π G-AGM emulates ideal F , the ideal protocol for F.

AGM emulation with respect to a sub-protocol. Our definitions of algebraic adversary and environment can be easily extended to the setting where the adversary/environment is restricted within a subprotocol, namely it can only use group elements in received from parties in this sub-protocol as its basis for algebraic representation. Definition 4. Suppose protocol ρ π involves group G, and π is a sub-protocol of ρ π . A pair of environment E and adversary A (in ρ π 's execution) is (G, π)-algebraic if it satisfies the following:

(1) A has a special output tape called the algebraic tape;

(2) Whenever A sends (backdoor, m) to some protocol machine, where m contains some X ∈ G, then either (1) A also writes an algebraic representation (with respect to π) of X on its algebraic tape, or (2) A has previously received such representation from E; where the algebraic representation of X is a list Λ = [(X 1 , λ 1 ), . . . , (X k , λ k )] (where X 1 , . . . , X k ∈ G and λ 1 , . . . , λ k ∈ Z p ) such that X = X λ1 1 • • • X λ k k , and X 1 , . . . , X k is the ordered list of group elements in messages E and/or A have received up to that point from either the environment or protocol machines in π, that is, excluding protocol machines in ρ π \ π. (For the formal definition of a "sub-protocol," see Appendix B.1 .)

Clearly, Definition 1 can be viewed as Definition 4 in the special case that ρ π = π. Note that now we can talk about AGM emulation with respect to a sub-protocol, i.e., protocol ρ π (G, π, φ)-AGM emulates ρ φ , where the environment/adversary pair is restricted by the sub-protocol π, and the environment/ simulator pair is restricted by the sub-protocol φ. The formal definition exactly follows Definition 2.

The algebraically dummy adversary. Similar to the standard UC framework, we can also define a notion of dummy adversary here; this will be usful in our protocol analyses in the later sections. Recall that in the standard UC framework, the dummy adversary is one that merely passes messages to and from the environment. However, in our setting, the environment might send some algebraic representations to the adversary, which we do not want the protocol parties to receive. Hence, we define the algebraically dummy adversary as dropping these algebraic representations. Definition 5. Suppose protocol π involves group G. An adversary D (in π's execution) is (G, π)-algebraically dummy if it satisfies the following: for any message (backdoor, m) sent from some identity ID = 0 (i.e., from some protocol machine), it sends (backdoor, (ID, m)) to the environment E; for any message (input, (ID, m)) sent from E, it sends (backdoor, m) to identity ID, except that if m contains X ∈ G and its algebraic representation Λ, then A sends (backdoor, m ) to identity ID instead, where m is m with Λ deleted.

Since D does not write anything on its algebraic tape, for (E, D) to be algebraic, E must send all necessary algebraic representations to D. To simplify notations, we may say "E is algebraic" in this case. Now we can define AGM emulation with respect to the dummy adversary: Definition 6. Suppose protocols π and φ involve the same group G. π G-AGM emulates φ with respect to the dummy adversary if the following holds: there is an efficient simulator S such that: for any efficient and (G, π)-algebraic environment E, we have that (E, S) are (G, φ)-algebraic, and

exec φ,S,E ≈ exec π,D,E ,
where D is the (G, π)-algebraically dummy adversary.

Similar to the standard UC framework, we can show that emulation is equivalent to emulation with respect to the dummy adversary. This simplifies protocol analysis, since from now on we can simply assume that the adversary is algebraically dummy. Theorem 1. Suppose protocols π and φ involve the same group G. Then π G-AGM emulates φ (as in Definition 2) iff π G-AGM emulates φ with respect to the dummy adversary (as in Definition 6).

The proof is tedious and is therefore deferred to Appendix B.3.

Composition in the UC-AGM

The composition theorem. We are now ready to prove the composition theorem in our UC-AGM framework: Theorem 2. Suppose protocols π and φ involve the same group G, such that φ is a sub-protocol of ρ φ , π G-AGM emulates φ, and π is identity-compatible with ρ φ and φ. Then ρ π (ρ φ with its sub-protocol φ replaced with π) (G, π, φ)-AGM emulates ρ φ . (For formal definitions of "identity-compatibility" and "sub-protocol replacement", see Appendix B.1) Proof. Let D π be the algebraically dummy adversary in an execution of π. Since π G-AGM emulates φ, we know that there is an efficient simulator S π such that: for any efficient and (G, π)-algebraic environment E π , we have that (E π , S π ) are (G, φ)-algebraic, and exec φ,Sπ,Eπ ≈ exec π,Dπ,Eπ .

Let ρ = ρ φ \ φ, i.e., ρ is the "caller" part of ρ π .

Construction of simulator S. By Theorem 1, it suffices to consider the (G, π)-algebraically dummy adversary D in an execution of ρ π . We construct a simulator S (in an execution of ρ φ ) which simulates E's view for any efficient and (G, π)-algebraic environment E. S essentially "combines" D and S π . Concretely, S works as follows:

1. On message (input, (ID, m 0 )) from identity 0 (recall that this means that E instructs S to send message m 0 to the protocol party with identity ID), S checks if there is a machine in φ with identity ID.

(a) If so, then S activates S π with input (input, (ID, m 0 )) (as from the environment), and follows S π 's instruction until the activation of S π completes. (b) Otherwise, i.e., ID is the identity of a machine in ρ, S parses m 0 = (m 0 , Λ) (where Λ is the algebraic representations of the group elements in m 0 ) and sends (backdoor, m 0 ) to ID, and writes Λ on its algebraic tape. 2. On message (backdoor, m 1 ) from some identity ID = 0 (i.e., from a protocol party), S checks if there is a machine in φ with identity ID.

(a) If so, then S activates S π with input (backdoor, m 1 ) (as from ID), and follows S π 's instruction until the activation of S π completes. (b) Otherwise, i.e., ID is the identity of a machine in ρ, S sends (backdoor, m 1 ) to identity 0 (i.e., to E).

Analysis of simulator S. It is straightforward to see that if S π is efficient, then S is also efficient. We now show that (E, S) are (G, φ)-algebraic. Recall that (E, S) are (G, φ)-algebraic iff whenever S sends (backdoor, m) to identity ID = 1, it also writes on its algebraic tape the algebraic representations (w.r.t. φ) of all group elements in m. According to the description of S above, S sends backdoor messages to identity ID = 1 in step 1(b) only; in this case S writes the algebraic representation Λ on its algebraic tape, so E is (G, π)-algebraic implies that (E, S) are (G, φ)-algebraic.

Moreover, S plays the role of an (G, π)-algebraic environment when activating S π with message (input, (ID, m 0 )). This is because S copies E's message payload m 0 , so E is (G, π)-algebraic implies that m 0 contains the algebraic representations (w.r.t. π) of its all group elements.

Next we show the validity of S. We construct another environment E π , which aims to distinguish between π's execution with D and φ's execution with S π . E π simulates instances of E and runs the codes of ρ and S locally, and essentially "combines" E, ρ, and S. Concretely, E π , on initial input z, activates E with initial input z. Then E π works as follows:

1. When E completes this activation, (a) If E halts with some output, then E π also halts with the same output. (b) If E generates an outgoing message (input, m 0 ) to some identity ID such that there is a machine µ ∈ ρ with identity ID, then E π runs the code of µ on message (input, m 0 ). When µ halts, ( * ) i. If µ generates an outgoing message (subroutine-output, m 1 ) to identity 0, then E π activates E with message (subroutine-output, m 1 ) (as from ID) and jumps to the beginning of this step. ii. If µ generates an outgoing message (backdoor, m 1 ) to identity 1, then E π runs the code of S on message (backdoor, m 1 ).

iii. If µ generates an outgoing message (input, m 1 ) to identity ID , which is the identity of a machine µ ∈ ρ, then E π runs the code of µ on input (input, m 1 ) and jumps to ( * ) (with µ replaced by µ ). iv. If µ generates an outgoing message (input, m 1 ) to identity ID , which is the identity of a machine in φ/π, then E π sends (input, m 1 ) to identity ID . (c) If E generates an outgoing message (input, (ID, m 0 )) to identity 1, then E π runs the code of S on message (input, (ID, m 0 )). 2. When S halts (as in case (b)ii or (c) in step 1; recall that S is a piece of code run by E itself), (a) If S generates an outgoing message (backdoor, m 2 ) to identity 0, then E π activates E with message (backdoor, m 2 ) and jumps to step 1. (b) If S generates an outgoing message (backdoor, m 2 ) to identity ID, which is the identity of a machine µ ∈ ρ, then E π runs the code of µ on message (input, m 2 ) and jumps to ( * ). (c) If S activates S π5 with message (input, (ID, m 2 )), then E π sends (input, (ID, m 2 )) to identity 1 (i.e., to D π or S π ). 3. On message (backdoor, (ID, m 3 )) from identity 1, E π runs the code of S on message (backdoor, (ID, m 3 ))

(as from S π ) and jumps to step 2. 4. On message (backdoor, m 3 ) from some identity ID = 1 (i.e., from a machine in φ or π) aimed at some identity ID , (a) If there is a machine µ ∈ ρ with identity ID , then E π runs the code of µ on message (input, m 3 ) and jumps to ( * ) (with µ replaced by µ ). (b) Otherwise, i.e., if ID is an external identity, then E π activates E with message (backdoor, m 3 ) (as from ID) and jumps to step 1.

It is straightforward to see that if E is efficient, then E π is also efficient. Also, E π perfectly simulates an instance of D in π's execution, and an instance of S π in φ's execution, i.e., exec π,Dπ,Eπ = exec ρ π ,D,E , and exec φ,Sπ,Eπ = exec ρ φ ,S,E .

Next we claim that if E is (G, π)-algebraic, then E π , as the environment in an execution of π, is also (G, π)-algebraic. Recall that E π is (G, π)-algebraic iff whenever it sends (input, m) to identity 1, m contains the algebraic representations (w.r.t. π) of its all group elements. According to the description of E π above, E π sends input messages to identity 1 in step 2(c) only. The message payload m 2 is copied from S's message aimed at S π ; we have argued above that S plays the role of a (G, π)-algebraic environment while communicating with S π , which implies that m 2 contains the algebraic representations (w.r.t. π) of its all group elements.

Since E π is both efficient and (G, π)-algebraic, by the definition of S π , we have that exec φ,Sπ,Eπ ≈ exec π,Dπ,Eπ .

Combining the three results above, we conclude that

exec ρ φ ,S,E ≈ exec ρ π ,D,E , completing the proof.
Transitivity of AGM-emulation. The following theorem is straightforward to prove, similarly to the standard UC framework.

Theorem 3. Suppose protocols π, π , φ involve the same group G, such that π G-AGM emulates π and π G-AGM emulates φ. Then π G-AGM emulates φ.

Proof. Our goal is to give a simulator S such that exec φ,S,E ≈ exec π,A,E when (E, A) are (G, π)-algebraic. Furthermore, (E, S) must be (G, φ)-algebraic.

By assumption, since π AGM-emulates π , there is an efficient algebraic adversary A such that exec π ,A ,E ≈ exec π,A,E when (E, A) are (G, π) algebraic. Furthermore, (E, A ) are (G, π )-algebraic.

Moreover, since π AGM-emulates φ, there is an efficient algebraic adversary S such that exec φ,S,E ≈ exec π ,A ,E when (E, A ) are (G, π )-algebraic. Furthermore, (E, S) are (G, φ)-algebraic. This implies that S is the required simulator, which concludes the proof.

In the standard UC framework, the guarantees given by the UC composition theorem can be plugged in as hypothesis of the transitivity theorem, which allows deriving a natural corollary when φ is an ideal functionality. Intuitively, in the standard UC setting, composition allows us to derive that ρ π emulates ρ F , when π emulates F. If, in turn ρ F has been shown to emulate F , then transitivity yields that ρ π emulates F .

However, this is not the case in the UC AGM setting. The composition theorem guarantees that ρ π emulates ρ F with respect to (G, π)-algebraic attackers, rather than (G, ρ π )-algebraic attackers. This means that, in order to plug-in composition results with transitivity to obtain a result for ideal functionality emulation, we require a refined theorem that considers the specific case of composed protocols.

Theorem 4. Suppose protocols ρ F , π and ideal functionalities F, F involve the same group G, such that: and4. π is identity-compatible with ρ F and ideal F .

1. ideal F is a sub-protocol of ρ F , 2. the π protocol (G, π)-AGM realizes F, 3. the ρ F protocol (G, ρ)-AGM realizes F ,
Then the instantiated protocol ρ π AGM realizes F with respect to attackers that are both (G, ρ)-and (G, π)-algebraic.

Proof (Sketch).

To prove this statement we need to recall the structure of the simulator for ρ π that is implied by the composition theorem; here we will call it A consistently with the transitivity theorem proof.

This simulator runs A internally and, when A communicates with machines executing π, it uses the simulator S π as a translator that communicates to F instead. On the other hand, communications between A and parties executing ρ are just passed along.

Note that, to use this simulator we need to apply the composition theorem, which means that (E, A) must be (G, π) algebraic; this is guaranteed by the stronger restriction that attackers are both (G, ρ) and (G, π) algebraic.

At this point we can now follow the same strategy adopted in the proof of the transitivity theorem: simulator A is used as an attacker against ρ F . The crucial observation now is that, this simulator guarantees that, if (E, A) are (G, π) algebraic and (G, ρ) algebraic, then (E, A ) is also (G, ρ) algebraic. This is because communications with ρ are just passed along between A and ρ.

We can now apply the hypothesis that the ρ F protocol (G, ρ)-AGM realizes F and take simulator S implied by this hypothesis to conclude the proof.

Extension to the full UC framework and relation to UC proofs. In Appendix B.2 we explain how our treatment here can be extended to the full UC framework, which models fully dynamic and evolving distributed computing systems.

UC emulation implies AGM emulation. For completeness, we note that UC emulation implies AGM emulation whenever the algebraic restriction on the simulator is moot. To see this, fix protocols π, φ where π UC emulates φ and φ does not impose any algebraic restriction on S. Any efficient algebraic environment E is in particular an efficient environment, so there is an efficient simulator S for which exec φ,S,E ≈ exec π,D,E holds for any efficient algebraic environment E. Furthermore, S is trivially algebraic since there is no such requirement when interacting with φ.

In Appendix E we discuss in detail how UC AGM proofs compose with stronger standard UC emulation results, and further clarify the implications of the UC AGM composition theorems. The discussion also clarifies what happens in the setting where different groups are used by different protocols.

We finally note that the fact that we refer to protocols that use the same group in our theorems because this is the more problematic case, and it serves to highlight the limitations to composition in the AGM. All our results carry without change to the case where different groups are used; in this case excluding attacks that prevent using group elements occurring in one protocol in an attack against another protocol, unless a representation can be provided, seems less of a limitation.

Analysis of the Chou-Orlandi Protocol

In this section, we analyze the security of the Chou-Orlandi protocol for oblivious transfer in the UC-AGM. For convenience, we present the standard OT functionality F OT in Figure 3. We describe the Chou-Orlandi protocol Π CO in Figure 4. All messages sent in the protocol are via a message authentication functionality F AUTH , as presented in [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]. -On input (send, sid , m0, m1) where m0, m1 ∈ {0, 1} from S do: if no message of the form (send, sid , m0, m1) has been stored, store (send, sid , m0, m1). -On input (deliver, sid , R) from S: if both (receive, sid , b) and (send, sid , m0, m1) have previously been stored, do:

• If R is honest: output (output, sid , m b ) to R. • If R is corrupted: output (output, sid , m b ) to S. Otherwise, output ⊥ to S.
-On input (deliver, sid , S) from S, if (output, sid , m b ) was previously output (to R or to S) and S is honest, output (output, sid ) to S. Otherwise, output ⊥ to S. We now turn toward proving security of the protocol. In the following, we denote S and R as the sender and the receiver in protocol Π CO , respectively. We describe a simulator Sim CO for Π CO by considering the different options for the order of corruptions. We assume that the simulator immediately aborts if it obtains syntactically ill-formed messages from a corrupted party as part of Π CO . We first give an outline of the proof.

Proof intuition. Roughly speaking, our proof must overcome two main challenges from the original work of Chou and Orlandi. The first is how to simulate the internal state of parties upon adaptive corruption. Namely, in Chou and Orlandi's proof, there seems to be no way of of explaining the secret exponent x chosen by R if S is statically corrupted and can send an arbitrary group element A in Step 1 for which R does not know the discrete logarithm y. This issue is easily resolved using the AGM, as the simulator always learns the exponent y from the algebraic coefficients provided for A.

The second issue in their proof comes from an improperly defined F OT functionality. Roughly speaking, their version of this functionality does not notify S upon R obtaining the message m b . If the corrupted R never makes the query for one of the keys k b to H then the simulator cannot extract the correct bit and complete the simulation of the protocol. Note that this issue cannot be overcome by the simulator naively completing the simulation before R makes this query by prompting the message (output, sid ) from F OT to S prematurely via a query on some arbitrary b. The reason is that E can always make the opposite query to H, i.e., for k 1-b , with probability 1 after the simulation is complete. In this case, there is no way to obtain m 1-b from F OT again, since S already had to make the query in order to force (output, sid ) being output to E. Both of these issues can be overcome when requiring that the environment E be algebraic. In this case, y is revealed when the corrupted S sends it in Step 1. For the issue of extraction, S observes that R sends U := A b g x . In the either case (i.e., b = 0 or b = 1), S can safely carry out the extraction for b. The only way for E to distinguish the simulation from the real world is by making a query from which a discrete logarithm instance can be solved (using algebraic coefficients provided by E as part of that query to H).

Let g denote a generator for a cyclic group G of prime order q and let DL denote the problem of computing a when given a random element A = g a in G. Moreover, denote Adv DL B := Pr[a = a | a ← B(g a )] the advantage of adversary B in solving DL. Then Theorem 5 shows that the Π CO protocol for oblivious transfer AGM realizes F OT . Theorem 5. Π CO UC-realizes F OT in the F RO -hybrid model under adaptive corruptions. More precisely, there exists an algebraic simulator Sim CO for the algebraically dummy adversary D such that, for every algebraic environment E that makes at most q H queries to F RO , there exist attackers B 1 and B 2 running in roughly the same time as E, such that exec FOT,S,E ≈ exec Π CO ,D,E , with

≤ q H • (Adv DL B1 + Adv DL B2 ).
Proof. The simulator Sim CO is as follows:

S is corrupted before Step 1.

-R is corrupted before Step 2. In this case, there is nothing for Sim CO to simulate.

-R is corrupted between Step 2 and 4. In this case, R has received A ∈ G from S (but has not yet received e 0 , e 1 ). In addition, Sim CO learns y ∈ Z p s.t. A = g y . Sim CO samples u ← Z p and computes U := g u , which it sends to S. When R becomes corrupted, Sim CO learns b and sets sets x := u -yb. It outputs (b, x) to E. In addition, it simulates the random oracle H as described in the next subcase. -R is corrupted after Step 4. In this case, R receives A ∈ G at Step 2 and e 0 , e 1 at Step 4. In addition, Sim CO learns y ∈ Z p s.t. A = g y . Sim CO samples u ← Z p and computes U := g u , which it sends to S.

To program H, when E queries H on input (I, J) (together with the algebraic representations of I, J), Sim CO does as follows.

• It first checks whether H[I, J] = ⊥. In this case, it returns H[I, J]. Thus, assume in the following that E queries H on some input for the first time. In addition, for any fresh query I, J, assume that Sim CO sets H[I, J] to the value it returns.

• If the query is of the form H(g y , U y g y 2 •(-b) ) for b ∈ {0, 1}, Sim CO sets k b ← {0, 1} κ . It returns k b .
• Otherwise Sim CO samples k ← {0, 1} κ and returns k.

• After observing both A and U in the protocol, Sim CO also retroactively checks whether it has previously set

H[g y , U y g y 2 •(-b) ]. If so, it sets k b := H[g y , U y g y 2 •(-b)
]. Upon having received e 0 , e 1 from S, Sim CO samples m 0 , m 1 ← {0, 1} κ . For all b ∈ {0, 1} for which k b = ⊥ at this point, it sets k b ← {0, 1} κ and programs H[g y , U y g y 2 •(-b) ] = k b (it does not resample k b in case it has already been defined). It then sets m 0 := e 0 ⊕ k 0 , m 1 := e 1 ⊕ k 1 and inputs (send, sid , m 0 , m 1 ) and (deliver, sid , R) to F OT . This prompts the output (output, sid , m b ) to the honest R, since R has previously input (receive, sid , b) to F OT . When R is corrupted, Sim CO learns b and sets x := u -yb (mod q). It outputs (b, x, m b ) to E.

S is corrupted between Step 1 and Step 3. To simulate the behaviour of S, Sim CO samples y ← Z p and computes A := g y , B := g y 2 . It sends Claim. Sim CO does not abort except with probability 1 q H Adv DL B1 , where B 1 is an adversary that runs in roughly the same time as E.

A to R. When S is corrupted, Sim CO learns m 0 , m 1 . It outputs (y, m 0 , m 1 ) to E. -R
Proof. Sim CO aborts in this case only if the adversary queries g y , U y , and U y g -y 2 , as it queries g y , U y g y 2 •(-b) for both b = 0, b = 1 to H by assumption. In this case, we can construct B 1 as follows. On input a discrete logarithm challenge A = g y in game DL, B 1 samples i ∈ [q H ] uniformly at random and runs E.

It simulates the behavior of Sim CO by sending the element

A in Step 1. If E corrupts R, B 1 aborts. When E (controlling R) queries H on input A, J, Sim CO learns coefficients a, c s.t. J = g a A c . If J = A u , and v = 0, then B 1 sets k 0 ← {0, 1} κ and programs H[A, J] = k 0 . If v = 1, U = g u g y and hence U y = J = g a A c yields the equation y 2 + (u -c) • y -a = 0 (mod q). For v ∈ {0, 1}, B 1 obtains the equation (v -1) • y 2 + (u -b)
• y -a = 0 (mod q) for y. If either of the latter cases occurs during the ith query to H, B 1 solves the equation and outputs y. Since B 1 guesses q correctly with probability at least 1 q H and perfectly simulates the behavior of Sim CO up that point perfectly, the claim follows.

-R is corrupted between Steps 2 and 4. In this case, the simulation for R can be carried out as in the case where S is corrupted before Step 1. -R is corrupted after Step 4. In this case, R receives e 0 , e 1 from the corrupted sender S at Step 4.

The only difference to the case where S is corrupted before Step 1 is that that Sim CO knows y ∈ Z p s.t. A = g y from sampling it in the first part of the simulation (rather than learning it from the algebraic coefficients output by the corrupted S).

S is corrupted after Step 3. To simulate the behaviour of S, in Step 1, Sim CO samples y ← Z p and computes A := g y , B := g y 2 . It sends A to R.

-R is corrupted before Step 2. When R sends U ∈ G to S, Sim CO obtains algebraic coefficients provided by R such that U = A b g x for some b ∈ {0, 1}, x ∈ Z p . Sim CO inputs (receive, sid , b) and then (deliver, sid , R) to F OT . This prompts the output (output, sid , m b ) to Sim CO , since S is honest at this point and has previously input (send, sid , m 0 , m 1 ) to F OT . To simulate H on input (I, J), Sim CO does as follows.

• It first checks whether H[I, J] = ⊥. In this case, it returns H[I, J]. Thus, assume in the following that H is queried on some input for the first time. In addition, for any fresh query I, J, assume that Sim CO sets H[I, J] to the value it returns.

• For any query to H, Sim CO checks whether it is of the form H(g y , U y g y The proof of the following claim is almost identical to the one given for the case where S is corrupted between Step 1 and Step 3.

Claim. Sim CO does not abort in case the sender is corrupted after Step 3 except with probability 1 q H Adv DL B2 , and B 2 runs in roughly the same time as E.

As long as Sim CO does not abort, it perfectly simulates the behavior of a party in Π CO , as all outputs of the random oracle H are uniformly distributed in this case from the view of E. Moreover, Sim CO can consistently simulate the view of E. Finally, it is easy to see that all Sim CO can output algebraic representations of all elements that it outputs relative to group elements it receives as input, and hence Sim CO is algebraic. This concludes the proof.

Analysis of PAKE protocols: SPAKE2 and CPace

In this section we analyze the UC security of PAKE protocols SPAKE2 and CPace in the algebraic group model. We show that, modeling the hash functions used by these protocols as random oracles, they both achieve full UC security. The proofs are simpler than the ones we encountered in the literature for the UC and game-based security of the same protocols and they are based on standard (non-interactive) assumptions (we do not need gap assumptions). We use the standard definition of F pwKE from [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF][START_REF] Canetti | Universally composable password-based key exchange[END_REF] supporting multiple sessions Fig. 5.

Remark. Throughout the paper we present the simulators as running their own instances of the random oracle functionality used by the protocols, which means that we assume that the random oracle is local to the protocol [START_REF] Canetti | Universally composable security with global setup[END_REF]. However, in this section, we make it clear that none of the given simulators needs to program the random oracle functionality and, in the case of the SPAKE2 protocol, it does not even need to know which adversarial queries were made to the random oracle. These observations indicate that our proofs of security may carry over to a setting with global random oracle as in [START_REF] Camenisch | The wonderful world of global random oracles[END_REF][START_REF] Canetti | Practical UC security with a global random oracle[END_REF]. Providing a full formalization of the referred works in the AGM is beyond the scope of this paper; however, we believe that our formal approach will carry naturally to extensions of UC with global functionalities.

Remark. The SPAKE2 simulator does not need to program the common reference string and the CPace protocol does not use one (in addition to the group description). We also show for both protocols that the simulators are algebraic. This means that the UC-AGM composition applies to both protocols.

Functionality F pwKE

Upon receiving a query (NewSession, sid , P, P , pw, role) from party 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 S.

Upon receiving a query (TestPwd, sid , P, pw * ) from S: 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".

Upon receiving a query (NewKey, sid , P, K * ) from S: 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 uniformly at random. Finally, append K to record (sid , P, P , pw, role), mark it completed, and output (sid , K) to P . User Server

x ← ← Zq y ← ← Zq X ← g x Y ← g y X ← X • M pw X ← X / M pw Y ← Y / N pw Y ← Y • N pw K ← H(sid , U, S, X , Y , pw, Y x ) K ← H(sid , U, S, X , Y , pw, X y ) sid , U, S, pw ∈ P, crs = (G, M, N ) X Y
Fig. 6. The SPAKE2 protocol [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF]. The CRS includes the group description G, where |G| = q and two group elements M, N ∈ G sampled uniformly at random.

SPAKE2

Fig. 6 shows a SPAKE2 protocol execution between an user U and a server S. SPAKE2 is a two-pass protocol, where we assume the user plays the role of the initiator and the server that of the responder. Let SqDH denote the problem of computing g a 2 , when given a random element A = g a in G, and Adv SqDH B the probability that attacker B succeeds in solving this problem. Theorem 6 shows that SPAKE2 AGM realizes F pwKE assuming that SqDH and the discrete-logarithm problems are hard in G. Theorem 6. SPAKE2 AGM-emulates F pwKE in the (F RO , F CRS )-hybrid model under static corruptions. More precisely, there exists an algebraic simulator S for the (algebraic) dummy adversary D such that, for every efficient algebraic environment E creating at most q S sessions and placing at most q H queries to the random oracle, there exist attackers B 1 1 , B 2 1 , and B 2 running in roughly the same time as E such that exec pwKE,S,E ≈ exec spake2,D,E , where

≤ Adv DL B 1 1 + Adv DL B 2 1 + q H • Adv SqDH B2 + q S + 1 q .
Note, that the DL problem and the SqDH problems are equivalent when we consider algebraic attackers, so the theorem follows with a reduction to the DL problem even if the proof relies on an apparently stronger assumption.

We also remark that the structure of this proof is much simpler than the proof that SPAKE2 satisfies relaxed UC PAKE security [START_REF] Abdalla | Universally composable relaxed password authenticated key exchange[END_REF]. This is because, in the AGM, the password guessing event can be detected directly by the simulator (and hence by the reductions) and one does not need to rely on the random oracle to extract passwords in active attacks.

We give a sketch of the proof and provide the full proof in Appendix C .

Proof (Sketch). Simulator S is shown in Fig. 7. Recall that, whenever the dummy adversary is instructed to deliver a group element to an uncorrupted party, it will output on its auxiliary tape the algebraic representation of that element with respect to group elements that appear in the view of the environment. In this case, the bases for such representations include M, N and any messages X or Y produced by an uncorrupted party.

Simulation strategy. The simulator generates all messages of uncorrupted parties by raising either M or N to a random exponent. It does so because it does not know the corresponding password. The distribution of such messages is identical to those produced by honest parties in the real world, which are of the form g x M pw or g y N pw . The simulator then keeps track of whether the adversary is launching a passive attack or an active attack: where the former means that there exists another simulated session with a consistent view.

All passively attacked sessions are not interrupted by the simulator, which means that F pwKE will choose independent keys at the associated dummy parties' outputs.

For actively attacked sessions, the simulator checks if the delivered message was constructed as per the protocol and, if so, it extracts the password. All malformed messages cause the simulator to interrupt the session in the functionality by calling TestPw with pw =⊥. For well formed messages, the simulator queries TestPw on the extracted password and, if the password is correct, computes the correct key: this is possible because, even though the simulator does not know the correct exponent implicit in the simulated honest party's state, it knows the algebraic decomposition of the delivered message and this is well formed (this means it can compute the key as the adversary would). If the password is incorrect, the simulator generates a totally random key (this is ignored by the functionality if there are no corrupt parties involved in the session, but it is relevant otherwise as we discuss below).

The simulation is perfect for all sessions with well-formed messages and correct password guesses. It looks perfect for all other sessions, unless the attacker can query the random oracle on the group element that such a session would compute in the real world. Our proof shows that any such query can, with overwhelming probability, be used to solve the SqDH problem. Two important observations for the proof: i. the simulator never uses the random exponents it generates for the honest party messages to perform any computation; and ii. the simulator never constructs any group element for which it cannot provide an algebraic decomposition to bases g, M and N. The second observation guarantees that our simulator is an algebraic adversary as required by the composition theorem in Section 2.

Corrupt parties. Fig. 7 does not show explicitly the simulator's handling of sessions involving corrupt parties. In this case, the environment tells the simulator what the corrupt party should be doing, and the simulator does not keep the state of the corrupt party. Moreover, any group elements transmitted by the corrupt party come with their algebraic decomposition as above. Our simulator is structured to handle this case identically to the setting where the uncorrupted party is actively attacked while interacting with another uncorrupted party; we explain why this is the case in the detailed version of the proof provided in Appendix C . The proof below covers this scenario as a particular case.

Proof of simulator correctness. From this point on we consider only interactions involving uncorrupted parties. The first observation we make is that the distribution of the protocol messages produced by the simulator is identical to that occurring in the real world, even though they are constructed differently. It therefore remains to prove that the outputs of the ideal functionality match the distribution of the parties' outputs in the real world. We observe that the real and ideal worlds are identical until bad, where bad is defined as the event that a secret key that is selected uniformly at random by the functionality at the output of an uncorrupted party is inconsistent with the answer given by H to the adversary. This is because in all other cases the simulator programs the output of the ideal functionality consistently with the real world. This means formally that, for = Pr[exec pwKE,S,E ⇒ bad], we have exec pwKE,S,E ≈ exec spake2,D,E More precisely, we define event bad as the existence within the set of queries placed by E to the random oracle of a query (sid , P, P , X , Y , pw, Z) that is consistent with the trace of a session at an uncorrupted party, which accepted after a passive attack or after an active attack where the simulator did not place a correct TestPw query. We define now these conditions formally.

We say a random oracle query (sid , P, P , X , Y , pw, Z) is consistent with an initiator session π sid P if this instance was created following a NewSession query by E using pw and π sid P = ( • , (P, P , X , Y ), • , init). Similarly, the condition for responder session π sid P is π sid P = ( • , (P, P , X , Y ), • , resp). Note that the order of party identities in the trace determines the role of the party.

We say an initiator session π sid P accepted after a passive attack if it completed following a SendResp(P , P, sid , (Y , alg)) message from E, when π sid P = ( • , (P, P , sid , X , Y ), • , resp). We say a responder session π sid P accepted after a passive attack if it completed following a SendInit(P, P , sid , (X , alg)) message from E, when π sid P = ( • , (P, P , sid , X , Y ), • , init). All other sessions are considered to be under active attack. We reduce the probability of bad to SqDH. Intuitively, our reduction embeds the SqDH challenge A in the global parameters (M = A, N = A δ ) for δ sampled uniformly at random from Z q (this accounts for the 1/q term in the theorem statement). Suppose bad is first set for a random oracle entry that is consistent with a session accepted by an initiator session. The attacker delivered a message Y and an algebraic representation that we can see as [(a, g), (b, M), (c, N)]. The reduction can transform this algebraic representation into [(a, g), (b + δc, A)]. Let CDH(A, B) = g ab for A = g a and B = g b . This means that any problematic random oracle query will include a group element of the form

Z = CDH(A x-pw , g a A b+δ(c-pw) ) = CDH(A x-pw , g a ) • CDH(A x-pw , A b+δ(c-pw) )
where x was chosen by the reduction following the simulator code. Since the reduction can compute the first factor, we can recover

CDH(A, A) (x-pw)(b+δ(c-pw))
which means that the required SqDH solution can be recovered when (x -pw)(b + δ(c -pw)) = 0. The case of responders is similar, but we can only recover the SqDH result provided δ(y -pw)(b + δc -pw) = 0. The detailed proof given Appendix C bounds the probability that our reduction strategy fails using a statistical term and reductions B 1 1 and B 2 1 to the discrete logarithm problem. Once this possibility is excluded, we can reduce the probability of bad to SqDH. The detailed proof also includes the code for the algorithm B 2 that breaks SqDH if the bad event occurs. In this case, we know that the random oracle table will contain a solution to SqDH if the event bad has occurred. When the experiment terminates, B 2 therefore samples a random oracle query uniformly at random6 and looks for a consistent session. It could find one or two consistent sessions, where the latter case corresponds to a passive attack with matching passwords on both sides. In any case, it computes a candidate SqDH value using the appropriate initiator or responder-side formula we described above. If the randomly selected random oracle entry was the first to cause the bad event, the algorithm solves SqDH. This accounts for the q H multiplicative loss in the theorem statement.

Remark. The above proof strategy can be used almost without change for an alternative version of the protocol that does not include the password pw in the input to the key derivation hash. This has practical advantages, as the password need not be kept in memory after computing the outgoing message. This version of the protocol was introduced as SPAKE1 in [START_REF] Abdalla | Simple password-based encrypted key exchange protocols[END_REF], and it was previously not known that this protocol could achieve forward secrecy or UC security. The only point where the current proof would need to be modified is in the final computation of the SqDH solution: in the particular case of a passive attack there now could be two protocol instances at P and P with different passwords, but matching the same random oracle entry. In this case, the reduction would toss a coin and choose one of them at random to fix the password used to compute the SqDH solution. This adds only a factor of 2 to the final reduction step.

Furthermore, the same proof applies to both protocols when we can rely on a DDH oracle to the fixed basis A to look for the offending random oracle entry. In this case, we get a tight reduction to Strong SqDH for both protocols, i.e., the strong DH assumption adapted to the computation of g a 2 . Finally, the proof also applies to variants of the protocol discussed in [START_REF] Abdalla | Perfect forward security of SPAKE2[END_REF], whereby the CRS is defined as (M, N = M ), or when the CRS is simply the group description and (M, N ) = H(sid , U, S) and H is modeled as a random oracle.

CPace

Fig. 8 shows a CPace protocol execution between an user U and a server S. CPace is a two-pass protocol, where we assume the user plays the role of the initiator and the server that of the responder. We give a sketch of the proof here and provide the complete proof in Appendix D .

User Server

G ← H1(sid , U, S, pw) G ← H1(sid , U, S, pw)

x ← ← Zq y ← ← Zq X ← G x Abort if X = 1 Abort if Y = 1 Y ← G y K ← H2(sid , X, Y, Y x ) K ← H2(sid , X, Y, X y ) sid , U, S, pw ∈ P, crs = (G) X Y
Fig. 8. The CPace protocol [START_REF] Haase | AuCPace: Efficient verifier-based PAKE protocol tailored for the IIoT[END_REF]. CRS includes the group description G s.t. |G| = q.

Let InvCDH denote the problem of computing g 1/a when given a random element A = g a in G and let Adv InvCDH B denote the probability that attacker B solves this problem. Theorem 7 shows that CPace AGM realizes F pwKE if InvCDH is hard in G.

Theorem 7. CPace AGM-emulates F pwKE under static corruptions, in a hybrid model with the random oracle functionality. More precisely, there exists an algebraic simulator S for the (algebraic) dummy adversary D such that, for every efficient algebraic environment E creating at most q S sessions, querying H 1 at most q H1 times and querying H 2 at most q H2 times, there exists B 1 , 2 running in roughly the same time as E such that exec pwKE,S,E ≈ exec cpace,D,E , where

≤ q H1 • q H2 • Adv InvCDH B 1 , 2 ( ) + q 2 H1 + q S q .
Note that the InvCDH problem is equivalent to the DL problem when we consider algebraic attackers, so the theorem follows with a reduction to the DL problem even if the proof relies on this apparently stronger assumption.

Proof. (Sketch) Simulator S is shown in Fig. 9. The simulation strategy here is identical to that we adopt for the SPAKE2 proof, with the caveat that the simulator must learn the environment's queries to H 1 in order to extract the password in an active attack. (In this case, the bases for the algebraic representations of adversarially constructed messages include the outputs of the random oracle H 1 and any messages X or Y produced by an uncorrupted party.) Also here the simulator never generates any group element for which it cannot give an algebraic decomposition with respect to base g, and hence it is an algebraic adversary. The handling of corrupt parties is also the same.

Proof of simulator correctness. This part of the proof is also similar in structure to that of SPAKE2. We first eliminate some corner cases, where the distribution of real world and the ideal world views do not match, but are straightforward to bound using a statistical term; this includes collisions at the random oracle output. We then conclude that the real and ideal worlds are identical until bad, where bad is defined as the existence within the set of queries placed by E to H 2 of a query (sid , X, Y, Z) that is consistent with the trace of a session at an uncorrupted party, which accepted after a passive attack or after an active attack where the simulator did not place a correct TestPw query. We define now these conditions formally.

We say an H 2 query (sid , X, Y, Z) is consistent with an initiator session π sid P if π sid P = ( • , ( • , • , X, Y), • , init). Similarly, the condition for responder session π sid P is π sid P = ( • , ( • , • , X, Y), • , resp). We say an initiator session π sid P accepted after a passive attack if it completed following a SendResp(P , P, sid , (Y, alg)) message from E, when π sid P = ( • , (P, P , sid , X, Y), • , resp). Responder session π sid P accepted after a passive attack if it completed after a SendInit(P, P , sid , (X, alg)) message from E, when π sid P = ( • , (P, P , sid , X, Y), • , init). All other sessions are considered to be under active attack. Finally, we say a T 1 entry of the form (sid , P, P , pw) is consistent with an initiator (resp. responder) instance, if that instance was initialized by the environment in a NewSession query with (sid , P, P , pw, init) (resp. (sid , P , P, pw, resp)).

We bound the probability of bad in the ideal world using a sequence of games.

Guessing the RO entries that cause bad. We modify ideal world as follows: sample ( 1 , 2 ) uniformly at random in [q H1 ] × [q H2 ]. Then, if bad first occurs due to the i-th H 2 query such that i = 2 , abort. Furthermore, if the offending T 1 entry (i.e., the T 1 unique entry consistent with the session where the bad event was detected) is not the 1 -th one, abort. Clearly, we can still bound the probability of bad in the previous game with the pessimistic bound q H1 • q H2 • Pr[bad], where we only check for bad if the experiment has not aborted. We give in Appendix D a reduction B 1, 2 that solves the InvCDH problem whenever bad occurs in this modified game.

Final reduction. The reduction strategy is as follows. The generator returned by H 1 for the problematic session associated with the 2 -th password query is programmed to be A, the InvCDH problem instance. All messages generated by uncorrupted parties are generated as g x or g ŷ . All random oracle queries consistent with a session with trace (X, Y) and generator A include the key element Z satisfying the following equation:

Z = X dlog A (Y) = Y dlog A (X) = A (dlog A (X)•dlog A (Y))
Observing that dlog A (X) = dlog g (X)/dlog g (A) the equation can be re-written as:

Z = g dlog g (X)•dlog g (Y) dlog g A
In the simplest case of a passive attack, it is immediate that we recover the solution to the InvCDH problem if x • ŷ = 0, which we know to be the case. Now let us suppose the problematic case occurs with an actively attacked initiator session. Then we know that Y = g α A β and α = 0; otherwise this would be a correct password guess and the bad event could never have occurred for this session-recall the experiment would have aborted if H 1 did not program A as the output for the password associated with this session. We can therefore refine the equation above to:

Z = g x•(α+β•dlog g (A)) dlog g A = g x•α dlog g A +x•β
Again, the InvCDH solution can be recovered, as long as x = 0. The responder session case is identical.

Remark. As in the proof of SPAKE2, we could eliminate the q H2 factor in the reduction by using a DDH oracle to the fixed basis A to detect which of the entries in H 2 is consistent with the bad event; however, we would still be guessing the problematic H 1 query in order to program the hard problem instance, and the q H1 factor would remain.

Remark. In the proofs for SPAKE2 and CPace, we have seen that it is possible to have tighter reductions to a stronger gap assumption that excludes the need to guess an entry in the key derivation random oracle. However, we should also mention that in the algebraic group model, the gap versions of the SqDH and InvCDH assumptions are actually equivalent to the standard versions, provided that the reduction is able to give algebraic decompositions of all the elements queried to the DDH oracle. This is the case in our proofs, provided that the attacker is also required to give algebraic decompositions of the group elements it queries to the random oracle. Note that this is a requirement for algebraic environments in the UC AGM model, as explained in Section 2. The take away from this discussion is that our proof of SPAKE2 implies a tight reduction to SqDH in the algebraic group model for both SPAKE1 and SPAKE2 (SPAKE1 is the variant that does not include pw in the key derivation hash). The CPace proof implies a reduction to InvCDH in the AGM with a loss of q H1 .

A On using an ideal functionality to idealize a group

One can try to formalize the AGM within the UC framework by introducing an appropriate functionality F AGM that "forces" arbitrary algorithms to behave algebraically. For example, the functionality could generate a group G along with a group element g (that it gives to all parties), and then maintain a set D ⊆ G (initialized as D = {g}) containing the group elements that are currently "registered." Any party can check whether a group element h is registered by querying F AGM to see whether h ∈ D; a party can register a new group element h by sending h to F AGM along with a representation of h with respect to the elements that are currently registered, after which h will be added to D. This approach would have the advantage of leaving the UC framework itself unchanged; once an appropriate F AGM functionality is defined, one could work in the F AGM -hybrid model, while automatically inheriting existing composition theorems. Nevertheless, although we considered this approach we ultimately found it unsatisfactory for several reasons:

-This approach requires honest parties to be aware of the fact that they are working in the AGM; in particular, any protocol designed in this model would need to instruct honest parties that when they receive a group element h they must make a query to F AGM checking whether h is registered. While not a fundamental barrier, this is clunky and conceptually awkward, and does not match what would be done in a real-world protocol execution. -A more serious problem is that it is not technically clear how composition would work for the version of F AGM described above (and we did not see any reasonable way to define F AGM that circumvents this issue). Consider the case of a protocol relying on the oblivious-transfer functionality F OT . In the spirit of the AGM, any group elements h 0 , h 1 sent to F OT by the sender should be registered-but this seems to require F OT itself to query F AGM to check whether that is the case. The same problem arises, e.g., when relying on the random-oracle functionality, if we insist that only registered group elements can be queried to the random oracle. Resolving this issue would thus, at least, require modifying standard functionalities when working in the AGM; even worse, it would require functionalities to communicate with each other, something that is disallowed in the standard UC framework. -The preceding issue could perhaps be solved, at least partially, by making F AGM a global functionality [START_REF] Canetti | Universally composable security with global setup[END_REF].

This, however, is problematic because then the simulator is unable to learn the representations of group elements when they are registered, which seems to limit the applicability of working in the AGM to begin with.

For these reasons, we decided to reject the above in favor of our current approach, which adopts the standard AGM idea of restricting the classes of attackers, rather than changing the rules of the environments in which the attackers execute. This leads to simpler and easy to check proofs and it preserves the syntax of ideal functionalities and protocols.

B Further Details Regarding the UC-AGM

B.1 Detailed Description of the Simplified UC Framework

In this section, we give a detailed description of the (simplified) UC framework [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]Section 2]; see Appendix B.2 for discussion on the full UC framework.

Protocols. A protocol is treated as a set of machines, where each machine has a fixed program and a set of specifications telling it how to communicate and with whom. A machine can be viewed roughly as a "party," but machines can also be abstract computational entities such as ideal functionalities.

More concretely, a machine is a tuple µ = (ID, C, μ), where -ID is µ's identity, which is unchanged throughout an execution of the protocol.

-C is µ's communication set, which specifies the parties to which µ can send messages. 7 It consists of pairs of the form (ID i , L i ), where L i is either input, subroutine-output, or backdoor. If L i = input, then µ is allowed to send input to the machine with identity ID i (we say µ is a caller of ID i ); if L i = subroutine-output, then µ is allowed to send output to the machine with identity ID i (we say µ is a subroutine of ID i ). As we shall see soon, backdoor is reserved for information sent to and from the adversary in an execution of the protocol. μ is µ's program. A program can be formally defined via some fixed computational model, such as interactive Turing machines (ITMs) or random access machines (RAMs). For concreteness, in this work we use ITMs as the model of computation.

Definition 7. A protocol is a set of machines π = {µ 1 , . . . , µ n }, where µ i = (ID i , C i , μi ), with the following properties:

-The identity ID i of each machine is unique.

-If π contains a machine µ = (ID, , ) which is a caller of ID , then π also contains a machine µ = (ID , , ) which is a subroutine of ID.

-If π contains a machine µ = (ID , , ) which is a subroutine of ID, and π also contains a machine µ = (ID, , ),8 then µ is a caller of ID .

Every machine in a protocol π is either an internal machine or a main machine. A main machine is a machine that is a subroutine of an external identity.

For now we say that a machine is efficient if it halts within a number of steps polynomial in a global security parameter κ. (See Appendix B.2 for more discussion on this.) Protocol execution. We distinguish between a protocol and its execution. Let π = {µ 1 , . . . , µ n } be a protocol, where µ i = (ID i , C i , μi ). Without loss of generality, assume µ 1 , . . . , µ m (where m ≤ n) are π's main machines. In an execution of protocol π, two additional machines are added. One is the environment

E = 0, (ID j , input)} m j=1 ∪ {(1, input) , Ẽ ;
the other is the adversary

A = 1, {(ID i , backdoor)} n i=1 ∪ {(0, backdoor)} , Ã .
In other words, the environment E has identity 0, and can send inputs to all main machines of π, as well as the adversary; the adversary A has identity 1, and can send backdoor messages to all machines of π, as well as the environment. (We require that none of the identities of machines in π, nor π's external identities, is 0 or 1.) Furthermore, in an execution of π, we change C i to C i ∪ {(1, backdoor)}. That is, every machine in π is additionally allowed to send backdoor message to the adversary. An execution of π starts by running the environment E; in other words, E is activated. Then when machine µ wants to transmit some message m (with identity ID) to some identity ID together with a label (input, subroutine-output, or backdoor) as allowed by µ's communication set, the execution proceeds as follows:

-If µ = E, then m is added to the state of µ with identity ID , together with a sender identity chosen by E from π's external identities.

-If µ = E and ID corresponds to some machine µ in π, then m is added to the state of µ , together with the sender identity ID.

-If µ = E and ID is an external identity, then m is added to the state of E, together with the sender identity ID.9

After that, µ's activation completes and µ (or E, if ID is an external identity) is activated. If µ halts without sending any message, then E is activated. 10In the "plain" model, the adversary can modify any message as it wants. Restrictions on the adversary's ability can be modeled via adding suitable ideal functionalities (see below), such as the message authentication functionality and the secure message transmission functionality.

A message has four components: the sender identity, the (intended) receiver identity, the label, and the payload. For readability, we use (label, payload) to denote a message; when it is necessary to make the identity of the sender and/or receiver explicit, we may use the term "from/to (or aimed at) identity."

We use exec π,A,E to denote environment E's view in π's execution with A.

Protocol emulation. We are now ready to define UC emulation of a protocol. Roughly speaking, a protocol π emulates another protocol φ, if any efficient environment's view in an execution of π (for any efficient adversary) can be "simulated" in an execution of φ. Concretely, Definition 8. Protocol π emulates protocol φ if the following holds: for any efficient adversary A in π's execution, there is an efficient adversary S (called the simulator) in φ's execution, such that for any efficient environment E we have exec φ,S,E ≈ exec π,A,E .

An immediate observation is that if π emulates φ, then the number and identities of main machines they each have must be the same; otherwise the environment can distinguish trivially. (We say that π is compatible with φ.) Also note that both A and S have identity 1.

Party corruption. Party corruption must be modeled carefully; in particular, it must be accounted for by the environment somehow, since otherwise the simulator could simply corrupt all parties at the outset and then simulate somewhat trivially. We provide the following simple mechanism. A main machine R, called the record keeping machine, is added to the protocol. When the adversary sends a (backdoor, corrupt) message to a protocol machine µ, µ notifies R that it is corrupted. R maintains a list of all corrupted parties; upon query from the environment, R returns this list.

The two common corruption settings are adaptive corruption, where the adversary can corrupt a party at any time; and static corruption, where party corruption must happen at the outset (so a party remains either corrupted or uncorrupted throughout protocol execution). Static corruption can be modeled via modifying the code of R as follows: upon activation of the adversary, it can send R a set of parties to be corrupted; all subsequent corrupt messages sent to R are ignored.

Realizing an ideal functionality. The most common form of UC emulation is realizing an ideal functionality. That is, the protocol emulated is an ideal protocol ideal F consisting of an incorruptible internal machine called the ideal functionality F, and m main machines called dummy parties, which merely pass all messages between their external identities and F (recall that in a protocol execution, messages from/to an external identity eventually comes from/goes to the environment); in particular, they ignore all messages from the adversary (except for corrupt messages discussed above). Definition 9. Protocol π realizes ideal functionality F if π emulates ideal F .

Universal composition. The universal composition operation, which is the key concept behind the composition theorem, involves three protocols φ, ρ φ and π, with the following properties:

1. φ is a sub-protocol of ρ φ : that is, φ ⊂ ρ φ (recall that we simply treat a protocol as a set of machines), and φ is a protocol in itself. 2. π is compatible with φ: recall that this means that the number and identities of π's and φ's main machines are the same. 3. π is identity-compatible with φ and ρ φ : that is, no machine in π has the same identity as any machine in ρ φ \ φ.

It is easy to see that, given the three conditions above, ρ π := ρ φ \ φ ∪ π also forms a protocol which is compatible with ρ φ ; that is, in ρ φ we can replace the sub-protocol φ with π.

The following universal composition theorem is proven in [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]:

Theorem 8. Suppose protocols ρ φ , π, φ are such that φ is a sub-protocol of ρ φ , π emulates φ, and π is identity-compatible with ρ φ and φ. Then ρ π emulates ρ φ .

When an ideal protocol ideal F is a sub-protocol of ρ ideal F , we simplify the notation to ρ F and say that protocol ρ F is in the F-hybrid world.

B.2 The Full UC Framework

We explain the main differences between the simplified UC framework used in Section 2 and the full UC framework, as well as how our treatment of algebraic adversaries there can be extended to the full framework. Our discussion here is mostly informal; for a formal treatment, we refer the readers to [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF].

Running time. Recall that in Appendix B.1 we define a machine to be efficient if it halts within a number of steps polynomial in the security parameter. While helping keep the concept simple, this definition appears overly restrictive; for example, in an encryption scheme where the encryption algorithm is "efficient" in this sense, the length of plaintexts is a priori bounded.

A natural alternative approach is to replace the security parameter with the input length in the definition of efficient machines. However, in a distributed system where there are multiple interactive Turing machines, things are more subtle. In particular, if we define an efficient ITM as halting within a number of steps polynomial in its overall input length, then this does not place any realistic limit on its running time: since two ITMs may repeatedly send inputs to each other with increasing length, they may run infinitely even though they are both "efficient."

To resolve this issue, [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF] replaces input length with "runtime budgets." That is, every message is associated with a natural number called import; at any specific state, the runtime budget of an ITM is defined as the overall import of messages it has received so far minus the overall import of messages it has sent so far. An ITM is efficient if at any state, the number of steps it has taken is at most some polynomial of its runtime budget at this state. In essence, the import of an message can be viewed as a "token" that provides running time; these "tokens" are circulated around the system, but the total number is an invariant.

To make the definition of UC emulation meaningful, [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF] also considers only balanced environments, whose overall import to protocol machines never exceeds the overall import to the adversary. For more detailed discussion, see [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF]Section 4.2].

Sender and receiver identities. Recall that a message in Appendix B.1 consists of label, payload, sender identity, and receiver identity. There we assume that the identities of all parties are public. However, in a dynamic system, such assumption cannot be made; for example, it is possible that the sender only knows part of the receiver's identity, or the sender might even want to invoke a new machine as the receiver.

To this end, [START_REF] Canetti | Universally composable security: A new paradigm for cryptographic protocols[END_REF] adds two more fields (apart from the import discussed above) to the message: a forcedwrite flag f , and a reveal-sender-id flag r. If f = 1 then the receiver's identity must exactly match the one specified in the message, µ ; if no machine in the system has identity µ , then one with identity µ is invoked. If f = 0 then µ is interpreted as a predicate on identities, and the message is delivered to the earliest-invoked machine whose identity satisfies µ (if no machine's identity satisfies µ , then the message is not delivered). This mechanism allows for delivery of messages without knowing the receiver's full identity (by setting f = 0), as well as invocation of new machines (by setting f = 1). Finally, if r = 1 and the message is delivered, then the sender's identity is sent together with the message.

In an execution of a protocol, the environment E must set the forced-write flag f = 1, i.e., E must know the identities of all machines it communicates with, and is free to invoke new machines; the adversary A must set f = 0, i.e., A can only communicate with existing machines; the protocol parties must set f = 0 while sending backdoor messages, i.e., they cannot invoke a new adversary, and they must reveal their identities while sending messages by setting r = 1. 11Protocol sessions and ITIs. The model in Appendix B.1 implicitly assumes that the total number of protocol sessions is fixed in advance (where each session of each party is an ITM). In order to take into account the dynamic generation of protocol sessions, the full UC framework instead lets the entire protocol to be a single ITM, and assigns multiple session IDs within this ITM; every combination of protocol code/party ID/session ID, called an extended identity, determines an instance of ITM (ITI). A session s of protocol π (or (π, s)) is simply the set of ITIs with code π and session ID s. As discussed above, ITIs can be dynamically generated, which allows for dynamic generation of protocol sessions. An extended session (π, s) is the transitive closure of the invocation relation starting from the ITIs in session (π, s). ITIs in session (π, s) are also called the main parties of s; ITIs in extended session (π, s) (but not in s) are also called the sub-parties of (π, s).

To provide some form of "separation" among protocol sessions, we require that the protocol be subroutine respecting. Roughly speaking, this means that the only messages sent to any ITI in an extended session from the outside are input messages to some main party, and the only messages sent from any ITI in an extended session to an existing outside ITI are subroutine-output messages from some main party.

Compatibility requirements. In the simplified framework, we assume that the identities of all protocol machines are public. However, in the dynamic setting where new ITIs can be invoked by existing ITIs (who also picks the identities of the new ITIs), this is not necessarily the case, causing potential difficulties in simulation (e.g., the simulator in the proof of Theorem 2 needs to check if there is a machine in protocol φ with identity ID). To resolve this, we only consider protocols which are identity exposing; that is, each session s of protocol π provides to the adversary an interface in which, given an extended identity α, answers with a bit indicating whether α is the extended identity of some ITI in extended session (π, s).

All the modifications to the simplified UC framework discussed above are orthogonal to our UC-AGM framework, so our treatment naturally extends to the full UC framework. The only exception is the running time, since our framework requires the environment and the adversary to additionally send (or output) the algebraic representations of group elements. However, notice that at any state of protocol execution, the length of algebraic representations sent/output by the environment/adversary cannot exceed the overall import it receives so far multiplies the length of the message (without the algebraic representations) it outputs this time. Therefore, if we replace all polynomials T (•) upper-bounding the running time with T (•) 2 (and let the environment assign imports appropriately), then the conclusions in the simple framework can be transferred to the full framework.

B.3 Proof of Theorem 1

Proof. For the "only if" direction, simply take Definition 2 and let A be the (G, π)-algebraically dummy adversary (which is clearly efficient assuming that the environment and all protocol machines are efficient).

For the "if" direction, let D be the (G, π)-algebraically dummy adversary. Since π G-AGM emulates φ w.r.t. the dummy adversary, we know that there is an efficient simulator S D such that (E , S D ) is (G, φ)algebraic, and exec φ,S D ,E ≈ exec π,D,E

for any efficient (G, π)-algebraic environment E .

Construction of simulator S. Given an efficient adversary A (in π's execution), we construct a simulator S (in φ's execution) which simulates E's view for any efficient environment E such that (E, A) is (G, π)algebraic. S simulates instances of both A and S D , and essentially "combines" them. (Recall that both A and S D communicate with the environment and protocol parties, and S needs to simulate all these interfaces.) Concretely, S works as follows:

1. On message (input, m 0 ) from identity 0 (i.e., from E), S (locally) activates A with message (input, m 0 ). 2. When A completes this activation, (a) If A does not generate any outgoing message, then S jumps to step 1. (b) If A generates an outgoing message (backdoor, m 1 ) to identity 0 (i.e., to the environment), then S sends (backdoor, m 1 ) to identity 0 (i.e., to E) and jumps to step 1. (c) If A generates an outgoing message (backdoor, m 1 ) to some identity ID = 0 (i.e., to a protocol machine), then S extracts Λ 1 as the concatenation of the algebraic representations of all group elements in m 1 , from either A's algebraic tape or messages previously sent to A. Then S (locally) activates S D with message (input, (ID, m 1 ||Λ 1 )). 3. When S D completes this activation, (a) If S D generates an outgoing message (backdoor, (ID, m 2 )) to identity 0 (i.e., to the environment), then S sends (backdoor, (ID, m 2 )) to identity 0 and jumps to step 1. (Note that A is "bypassed" in this case.) (b) If S D generates an outgoing message (backdoor, m 2 ) to some identity ID = 0 (i.e., to a protocol machine), then S extracts Λ 2 as the concatenation of the algebraic representations of all group elements in m 2 , from either S D 's algebraic tape or messages previously sent to S D . Then S writes Λ 2 on its own algebraic tape and sends (backdoor, m 2 ) to identity ID. 4. On message (backdoor, m 3 ) from identity ID = 0 (i.e., from a protocol machine), S activates S D with message (backdoor, m 3 ). 5. When S D completes this activation, (a) If S D generates an outgoing message (backdoor, (ID, m 2 )) to identity 0, then S activates A with message (backdoor, (ID, m 2 )) and jumps to step 2. (b) If S D generates an outgoing message (backdoor, m 2 ) to some identity ID = 0 (i.e., to a protocol machine), then S extracts Λ 2 as the concatenation of the algebraic representations of all group elements in m 2 , from either S D 's algebraic tape or messages previously sent to S D . Then S writes Λ 2 on its own algebraic tape and sends (backdoor, m 2 ) to identity ID. (Note that the only difference with step 3 is that in case (a) A is not "bypassed.") Analysis of simulator S. It is straightforward to see that if A and S D are both efficient, then S is also efficient. We now show that (E, S) is (G, φ)-algebraic in two steps:

-Recall that while interacting with S D , S generates the interfaces of both the environment and protocol parties in the execution of φ. Let E denote such environment in S D 's view; we show that E is (G, π)algebraic. E sends an input message to identity 0 (i.e., the adversary) in step 2(c) only (let m 1 be the message payload), in which case an algebraic representation Λ 1 is attached to m 1 . Such an algebraic representation can be extracted because (E, A) is (G, π)-algebraic, so (1) if Λ 1 is on A's algebraic tape, then it can be read by S; (2) otherwise Λ 1 must have been previously sent to A by S (who simulates E in A's view), so S can extract Λ 1 from its own transcript.

-Since E is (G, π)-algebraic, by definition of S D , we have that (E , S D ) is (G, φ)-algebraic. Now we claim that (E, S) is (G, φ)-algebraic. S sends (backdoor messages to identity ID = 1 in steps 3(b) and 5(b) only (let m 2 be the message payload); in both cases S writes an algebraic representation Λ 2 on its algebraic tape. Such an algebraic representation can be extracted because (1) if Λ 2 is on S D 's algebraic tape, then it can be read by S;

(2) otherwise Λ 2 must have been previously sent to S D by E , which in turn is part of S, so S can extract Λ 2 from its own transcript.

Next we show that S generates an indistinguishable view for E. We construct another environment E D , which simulates instances of both E and A, and essentially "combines" them. Concretely, E D , on initial input z, activates E with input z. Then E D works as follows: to identity 1 (i.e., to the adversary).12 3. On message (backdoor, (ID, m 2 )) from identity 1 (i.e., from the adversary), (a) If E D is in the bypass state, then it exits this state, activates E with message (subroutine-output, (ID, m 2 )) (as from identity 1), and jumps to step 1. (b) Otherwise E D activates A with message (input, m 2 ) (as from identity ID) and jumps to step 2, except that in case 2(b) E D activates E with message (backdoor, m 1 ) (rather than entering the bypass state). 4. On message (subroutine-output, m 3 ) from identity ID = 1 (i.e., from a protocol machine), E D activates E with message (subroutine-output, m 3 ) and jumps to step 1.

It is straightforward to see that if E and A are both efficient, then E D is also efficient. Also, E D perfectly simulates an instance of A in π's execution, and an instance of S in φ's execution, i.e., Next we claim that if (E, A) is (G, π)-algebraic, then E D is also (G, π)-algebraic. According to the description of E D above, E D sends input messages to identity 1 in step 2(c) only (let m 1 be the message payload), in which case an algebraic representation Λ is attached to m 1 . Such an algebraic representation can be extracted because (E, A) is (G, π)-algebraic, so (1) if Λ is on A's algebraic tape, then it can be read by E D ;

(2) otherwise Λ must have been previously sent to A by E, so E D , who runs both E and A, can extract Λ from the message sent from E to A.

Since E D is both efficient and algebraic, by the definition of S D , we have that

exec φ,S D ,E D ≈ exec π,D,E D .
Combining the three results above, we conclude that exec φ,S,E ≈ exec π,A,E , completing the proof.

C Detailed Proof for SPAKE2 (Theorem 6)

Simulator S is shown (again) in Fig. 10, side by side with the code for uncorrupted parties in the real-world.

Recall that, whenever the dummy adversary is instructed to deliver a group element to an uncorrupted party, it will output in its auxiliary tape the algebraic representation of that element with respect to group elements appear in the view of the environment. In this case, the bases for such representations include M, N and any messages X or Y produced by an uncorrupted party.

Simulation strategy. The simulator generates all messages of uncorrupted parties by simpling raising either M or N to a random exponent. It does so because it does not know the corresponding password.

The distribution of such messages is identical to those produced by honest parties in the real world, which are of the form g x M pw or g y N pw . The simulator then keeps track of whether the adversary is launching a passive attack or an active attack, where the former means that there exists another simulated session with a consistent view. All passively attacked sessions are not interrupted by the simulator, which means that F pwKE will choose independent keys at the associated dummy parties' outputs. For actively attacked sessions, the simulator checks if the delivered message was constructed as per the protocol and, if so, it extracts the password. All malformed messages cause the simulator to interrupt the session in the functionality by calling TestPw with pw =⊥. For well formed messages, the simulator queries TestPw on the extracted password and, if the password is correct, computes the correct key: this is possible because, even though the simulator does not know the correct exponent implicit in the simulated honest party's state, it knows the algebraic decomposition of the delivered message and this is well formed (this means it can compute the key as the adversary would). If the password is incorrect, the simulator generates a totally random key (this is ignored by the functionality if there are no corrupt parties involved in the session, but it is relevant otherwise as we discuss below). The simulation is perfect for all sessions with well-formed messages and correct password guesses. It looks perfect for all other sessions, unless the attacker can query the random oracle on the group element that such a session would compute in the real world. Our proof shows that any such query can, with overwhelming probability, be used to solve the SqDH problem. Two important observations for the proof: i. the simulator never uses the random exponents it generates for the honest party messages to perform any computation; and ii. the simulator never constructs any group element for which it cannot provide an algebraic decomposition to bases g, M and N. The second observation guarantees that our simulator is an algebraic adversary as required by the composition theorem in Section 2.

Corrupt parties. Fig. 10 does not show explicitly the simulator's handling of sessions involving corrupt parties. In this case, the environment tells the simulator what the corrupt party should be doing, and the simulator does not keep the state of the corrupt party. Moreover, any group elements transmitted by the corrupt party come with their algebraic decomposition as above.

In particular, this means that any output key produced by a corrupt party can be easily fixed by the simulator at the ideal functionality output, since its intended real-world output will be explicitly provided by the environment. More subtle is the case of sessions accepted by uncorrupted parties when interacting with corrupt parties: in this case the simulator must also fix the output of the uncorrupted party via the ideal functionality consistently with the real world.

Our simulator is structured to handle this case identically to the setting where the uncorrupted party is actively attacked while interacting with another uncorrupted party:

such a session will never be interpreted as passively attacked by the simulator (as it is not controlling the corrupt party state), so it will always test the password; if the password is correctly guessed, our simulator programs the functionality with the correct key; otherwise, it programs a completely random key (mimicking actively attacked sessions); in both cases the functionality outputs what the simulator provides because the session is corrupted.

The proof below covers this scenario as a particular case.

Proof of simulator correctness. From this point on we consider only interactions involving uncorrupted parties. The first observation we make is that the distribution of the protocol messages produced by the simulator is identical to that occurring in the real world, even though they are constructed differently. It therefore remains to prove that the outputs of the ideal functionality match the distribution of the parties' outputs in the real world. We observe that the real and ideal worlds are identical until bad, where bad is defined as the event that a secret key that is selected uniformly at random by the functionality at the output of an uncorrupted party is inconsistent with the answer given by H to the adversary. This is because in all other cases the simulator programs the output of the ideal functionality consistently with the real world. This means formally that, for = Pr[exec pwKE,S,E ⇒ bad], we have exec pwKE,S,E ≈ exec spake2,D,E More precisely, we define event bad as the existence within the set of queries placed by E to the random oracle of a query (sid , P, P , X , Y , pw, Z) that is consistent with the trace of a session at an uncorrupted party, which accepted after a passive attack or after an active attack where the simulator did not place a correct TestPw query. We define now these conditions formally.

We say a random oracle query (sid , P, P , X , Y , pw, Z) is consistent with an initiator session π sid P if this instance was created following a NewSession query by E using pw and π sid P = ( • , (P, P , X , Y ), • , init). Similarly, the condition for responder session π sid P is π sid P = ( • , (P, P , X , Y ), • , resp). Note that the order of party identities in the trace determines the role of the party.

We say an initiator session π sid P accepted after a passive attack if it completed following a SendResp(P , P, sid , (Y , alg)) message from E, when π sid P = ( • , (P, P , sid , X , Y ), • , resp). We say a responder session π sid P accepted after a passive attack if it completed following a SendInit(P, P , sid , (X , alg)) message from E, when π sid P = ( • , (P, P , sid , X , Y ), • , init). All other sessions are considered to be under active attack. We reduce the probability of bad to SqDH. Intuitively, our reduction embeds the SqDH challenge A in the global parameters (M = A, N = A δ ) for δ sampled uniformly at random from Z q (this accounts for the 1/q term in the theorem statement). Suppose bad is first set for a random oracle entry that is consistent with a session accepted by an initiator session. The attacker delivered a message Y and an algebraic representation that we can see as [(a, g), (b, M), (c, N)]. The reduction can transform this algebraic representation into [(a, g), (b + δc, A)]. This means that any problematic random oracle query will include a group element of the form

Z = CDH(A x-pw , g a A b+δ(c-pw) ) = CDH(A x-pw , g a ) • CDH(A x-pw , A b+δ(c-pw) )
where x was chosen by the reduction following the simulator code. Since the reduction can compute the first factor, we can recover CDH(A, A) (x-pw)(b+δ(c-pw))

which means that the required SqDH solution can be recovered when (x -pw)(b + δ(c -pw)) = 0. The case of responders is similar, but we can only recover the SqDH result provided δ(y -pw)(b + δc -pw) = 0. We therefore split the bad event into the following cases:

- bad 1 I,R : bad 1 first occurs because the value x (resp. y) sampled in an initiator (resp. responder) session matches the password pw that was included by E in the NewSession query that created that session. This event is easy to bound, as pw is fixed when the value is sampled, and it accounts for the q S /q term in the theorem statement.

bad 2 I : bad I first occurs because bad 1 I,R did not occur and c = pw. In the case of passive attacks, this means that the environment extracted the value y = c sampled by the simulator in the matching session. In active attacks, this can never occur. To see this, note that if bad occurs and c = pw, then it must be the case that b = 0, as otherwise the simulator would have made a correct password guess and computed the correct key. But then, the condition (b + δ(c -pw)) = 0 cannot be satisfied.

bad 2 R : bad R first occurs because none of the previous variants occurred and b = pw. In the case of passive attacks, this means that the environment extracted the value x = b sampled by the simulator in the matching session. In active attacks, this can never occur. To see this, note that if bad occurs and b = pw, then it must be the case that c = 0, as otherwise the simulator would have made a correct password guess and computed the correct key. But then, the condition (b + δc -pw) = 0 cannot be satisfied because we use δ = 0.

bad 3 I : bad I first occurs because none of the previous variants occurred and (b + δ(c -pw)) = 0. This event can only occur in actively attacked sessions, as passively attacked sessions all have b = 0 and bad 2 1 has not occurred.

bad 3 R : bad R first occurs because none of the previous variants occurred and (b + δc -pw) = 0. This event can only occur in actively attacked sessions, as passively attacked sessions all have c = 0 and bad 3 1 has not occurred.

It is straightforward to bound bad 2 I ∨ bad 2 R by reducing the probability of these events occurring to the discrete logarithm problem. Let us without loss of generality assume we get q S discrete logarithm challenges and use them as the messages X and Y produced by the simulator. The reduction defines (M = g λ , N = g δ ), for random λ and δ. Then, if bad 2 I occurs, we obtain the discrete logarithm c of some Y wrp to N, and we can compute the discrete logarithm to the base g as λ • c. The reasoning for the responder side is identical. We call this reduction B 1 1 in the theorem statement. We now consider the last two cases. We note that bad R that b = pw. These two events can be jointly reduced to the Discrete Logarithm problem by setting (M = g λ , N = R) where R is the discrete logarithm challenge and λ is sampled uniformly at random. Indeed, if either of these events occurs, then the reduction can recover δ, and consequently the discrete logarithm λ • δ (recall we have defined N = M δ ). We call this reduction B 2 1 in the theorem statement. Bounding bad 2 : reduction to SqDH. Fig. 11 gives the detailed reduction to SqDH. The reduction, as presented, would fail in the cases we have excluded with bad 1 , but here we can assume that bad 1 has not occurred. The reduction follows the strategy we outlined above. When the experiment terminates, it samples a random oracle query uniformly at random 13 and looks for a consistent session. It could find one or two consistent sessions, where the latter case corresponds to a passive attack with matching passwords on both sides. In any case, it computes a candidate SqDH value using the appropriate initiator or responder-side formula we described above. If the randomly selected random oracle entry was the first to cause the bad event, the algorithm solves SqDH. This accounts for the q H multiplicative loss in the theorem statement.

D Detailed Proof for CPace (Theorem 7)

Simulator S is shown (again) in Fig. 12, side by side with the code for uncorrupted parties in the real-world. Recall that, whenever the dummy adversary is instructed to deliver a group element to an uncorrupted party, it will output in its auxiliary tape the algebraic representation of that element with respect to group elements appear in the view of the environment. In this case the bases for such representations include the outputs of the random oracle H 1 and any messages X or Y produced by an uncorrupted party.

Simulation strategy and handling of corrupt parties. The simulation strategy here is identical to that we adopt for the SPAKE2 proof, with the caveat that the simulator must learn the environments' queries to H 1 in order to extract the password in an active attack. The handling of corrupt parties is also the same. Also here the simulator never generates any group element for which it cannot give an algebraic decomposition with respect to base g, and hence it is an algebraic adversary. The handling of corrupt parties is also the same.

Proof of simulator correctness. From this point on we consider only interactions involving uncorrupted parties. The first observation we make is that the distribution of the protocol messages produced by the simulator is statistically close to that occurring in the real world, even though they are constructed differently. The only difference is that we exclude the case where x or ŷ are zero. We therefore first modify the real-world so that the distribution of the protocol messages matches that of the ideal world. This explains the statistical term q S /q in the theorem statement. Moreover, the simulator will abort if at some point it cannot invert outputs of H 1 due to ambiguity in T 1 . The probability of abort explains the statistical factor of q 2 H1 /q in the theorem statement.

It remains to prove that the outputs of the ideal functionality match the distribution of the parties' outputs in this slightly modified version of the real world. We observe that the real and ideal worlds are now identical until bad, where bad is defined as the event that a secret key that is selected uniformly at random by the functionality at the output of an uncorrupted party is inconsistent with the answer given by H 2 to the adversary. This is because in all other cases the simulator programs the output of the ideal functionality consistently with the real world. This means formally that, for = Pr[exec pwKE,S,E ⇒ bad], we have exec pwKE,S,E ≈ exec cpace,D,E .

More precisely, we define event bad as the existence within the set of queries placed by E to H 2 of a query (sid , X, Y, Z) that is consistent with the trace of a session at an uncorrupted party, which accepted after a passive attack or after an active attack where the simulator did not place a correct TestPw query. We define now these conditions formally.

We say an H 2 query (sid , X, Y, Z) is consistent with an initiator session π sid P if π sid P = ( • , ( • , • , X, Y), • , init). Similarly, the condition for responder session π sid P is π sid P = ( • , ( • , • , X, Y), • , resp). We say an initiator session π sid P accepted after a passive attack if it completed following a SendResp(P , P, sid , (Y, alg)) message from E, when π sid P = ( • , (P, P , sid , X, Y), • , resp). Responder session π sid P accepted after a passive attack if it completed after a SendInit(P, P , sid , (X, alg)) message from E, when π sid P = ( • , (P, P , sid , X, Y), • , init). All other sessions are considered to be under active attack. Finally, we say a T 1 entry of the form (sid , P, P , pw) is consistent with an initiator (resp. responder) instance, if that instance was initialized by the environment in a NewSession query with (sid , P, P , pw, init) (resp. (sid , P , P, pw, resp)).

We bound the probability of bad in the ideal world using a simple sequence of games.

Guessing the RO entries that cause bad. We modify ideal world as follows: sample ( 1 , 2 ) uniformly at random in [q H1 ] × [q H2 ]. Then, if bad first occurs due to the i-th H 2 query such that i = 2 , abort. Furthermore, if the offending T 1 entry (i.e., the T 1 unique entry consistent with the session where the bad event was detected) is not the 1 -th one, abort. Clearly, we can still bound the probability of bad in the previous game with the pessimistic bound q H1 • q H2 • Pr[bad], where we only check for bad if the experiment has not aborted. We give in Fig. 13 a reduction B 1 , 2 that solves the InvCDH problem whenever bad occurs in this modified game.

Final reduction. The reduction strategy is as follows. The generator returned by H 1 for the problematic session associated with the 2 -th password query is programmed to be A, the InvCDH problem instance. All messages generated by uncorrupted parties are generated as g x or g ŷ . All random oracle queries consistent with a session with trace (X, Y) and generator A include the key element Z satisfying the following equation:

Z = X dlog A (Y) = Y dlog A (X) = A (dlog A (X)•dlog A (Y))
Observing that dlog A (X) = dlog g (X)/dlog g (A) the equation can be re-written as:

Z = g dlog g (X)•dlog g (Y) dlog g A
In the simplest case of a passive attack, it is immediate that we recover the solution to the InvCDH problem if x • ŷ = 0, which we know to be the case. Now let us suppose the problematic case occurs with an actively attacked initiator session. Then we know that Y = g α A β and α = 0; otherwise this would be a correct password guess and the bad event could never have occurred for this session-recall the experiment would have aborted if H 1 did not program A as the output for the password associated with this session. We can therefore refine the equation above to:

Z = g x•(α+β•dlog g (A)) dlog g A = g x•α dlog g A +x•β
Again, the InvCDH solution can be recovered, as long as x = 0. The responder session case is identical.

E Implications of UC AGM composability

In this section we give a more detailed discussion of the UC AGM model and the implications of our theorems.

The UC-AGM model deviates from the UC model in two ways:

it extends the execution model with one or more CRS functionalities for group definitions; and it constrains adversaries, environments and simulators to behave algebraically w.r.t. to said group descriptions.

We argue that any UC proof in the standard model implies, as expected, a proof in the UC-AGM model. This means that we can compose UC-secure protocols with UC-AGM protocols using the UC-AGM composition theorem. Moreover, we argue that UC-AGM emulation w.r.t. to different F CRS functionalities (possibly using the same mathematical group) also composes. These results create a hierarchy of UC emulation notions, all of which can be composed with each-other by further restricting the adversarial entities to be algebraic with respect to all groups used by the different protocols. We reinforce this last point: composition comes at the cost of weakening the overall claim to holding over algebraically restricted adversarial entities-combining results results in a more restrictive setting-which is the natural consequence of considering algebraic adversaries. We first give the high-level details and then demonstrate with examples.

Algebraic Contexts. Let us first distinguish adversarial machines from non-adversarial machines. The former include simulators, real-world adversaries, environments and corrupted protocol participants. The latter include ideal functionalities and honest protocol participants. The notion of an algebraic adversarial machine depends on the context in which this machine is executed. Fix a functionality F CRS , defining a group description G. Adversarial machines must behave algebraically w.r.t. to G whenever the bit strings they produce are interpreted (typed) as elements in G by the target non-adversarial machines-note that this applies only to group elements delivered via backdoor interfaces, but not to protocol inputs. Furthermore, these algorithms can only use as bases for their representations group elements that they read directly from F CRS or that they receive with this interpretation (type) from a non-adversarial machine. These interpretations must be fixed because proofs will rely on the restrictions that come as a consequence.

We call non-adversarial machines that never interpret an incoming or outgoing bit-string as an element in G as G-agnostic. More precisely, in a context where F CRS is present and provides a description of G, G-agnostic machines do not restrict adversarial machines into providing algebraic representations for group elements in G, nor do they produce group elements that can be used any adversarial entity as a basis for a representation of a group in G.

It is crucial that, for all machines in the context of a claim and all groups G in the same context, one defines a priori whether a machine is adversarial and, if not, whether it is G-agnostic. In the particular case of an ideal-world adversary S interacting with an ideal functionality, there is only one target non-adversarial machine. Intuitively, if S is interacting with an F that is G-agnostic, then S is trivially algebraic w.r.t. to G. For the particular case of F CRS defining G, we have that F CRS is agnostic to all other groups and it is not agnostic w.r.t. to G, as it provides the basis for group element representations.

UC emulation implies UC AGM emulation. Our first claim is that standard UC emulation w.r.t. a G-agnostic functionality implies UC emulation in the AGM w.r.t. to G.

Theorem 9 (Informal). Fix a protocol π that UC emulates G-agnostic functionality F. Then π UC emulates F w.r.t. G-algebraic adversarial machines.

Proof. (Sketch) Algebraic adversaries and environments are subclasses of general UC adversaries and environments, so an UC-AGM simulator S is guaranteed to exist for all algebraic environments and the dummy algebraic adversary; furthermore S is trivially algebraic because F is G-agnostic.

The same argument applies when we consider UC-AGM emulation with respect to two different groups. Suppose F is not G 1 -agnostic but it is G 2 agnostic. Suppose further than S is G 1 -algebraic when it interacts with F. Then S is trivially (G 1 , G 2 )-algebraic when it interacts with F. From here we obtain the following result.

Theorem 10 (Informal). Fix a protocol π that UC emulates a G 2 -agnostic functionality F w.r.t. G 1algebraic adversarial machines. Then π UC emulates F w.r.t. (G 1 , G 2 )-algebraic adversarial machines.

Combining these results with the AGM-UC composition theorem yields a comprehensive compositional framework.

Fig. 1 .

 1 Fig. 1. The AGM UC real and ideal worlds. Blue arrows impose algebraic behaviour.

Fig. 2 .

 2 Fig. 2. The UC AGM restrictions for composition (blue) and transitivity (blue/green).

FunctionalityFOT--

  On input (receive, sid , b) where b ∈ {0, 1} from R do: if no message of the form (receive, sid , b), b ∈ {0, 1} has been stored, store (receive, sid , b). Output (receive, sid ) to S. -On input (send, sid , m0, m1) where m0, m1 ∈ {0, 1} from S do: if no message of the form (send, sid , m0, m1) has been stored, store (send, sid , m0, m1). Output (send, sid ) to S. Adversary S: On input (receive, sid , b) where b ∈ {0, 1} from S do: if no message of the form (receive, sid , b), b ∈ {0, 1} has been stored, store (receive, sid , b).

Fig. 3 .-Step 1 :

 31 Fig. 3. Functionality for 1-out-of-2 OT

Fig. 4 .

 4 Fig. 4. The Chou-Orlandi OT protocol.

Fig. 5 .

 5 Fig. 5. The password-based key-exchange functionality F pwKE .

1 .

 1 When E completes this activation, (a) If E halts with some output, then E D also halts with the same output. (b) If E generates an outgoing message (input, m 0 ) to some identity ID = 0 (i.e., to a protocol machine), then E D sends (input, m 0 ) to identity ID. (c) If E generates an outgoing message (input, m 0 ) to identity 1 (i.e., to the adversary), then E D activates A with message (input, m 0 ). 2. When A completes this activation, (a) If A does not generate any outgoing message, then E D jumps to step 1. (b) If A generates an outgoing message (backdoor, m 1 ) to identity 0 (i.e., to the environment), then E D enters a special state called bypass. (c) If A generates an outgoing message (backdoor, m 1 ) to some identity ID = 0 (i.e., to a protocol machine), then E D extracts Λ as the concatenation of the algebraic representations of all group elements in m 1 , from either A's algebraic tape or messages previously sent from E to A. Then E D sends (input, (ID, m 1 ||Λ))

  exec π,D,E D = exec π,A,E , and exec φ,S D ,E D = exec φ,S,E .

  bad I : bad is first detected on an initiator session but (x -pw)(b + δ(c -pw)) = 0 -bad R : bad is first detected on a responder session but δ(y -pw)(b + δc -pw) = 0 -bad 1 = bad I ∨ bad R bad 2 = bad ∧ ¬bad 1 Clearly we have Pr[exec pwKE,S,E ⇒ bad] = Pr[exec pwKE,S,E ⇒ bad 1 ] + Pr[exec pwKE,S,E ⇒ bad 2 ] . Bounding bad 1 : Reductions to Discrete Log We analyze bad 1 by splitting it into five disjoint cases:

3 I

 3 occurs if and only if δ = b/(pw -c), as we know from bad 2 I that c = pw. Similarly, bad 3 R occurs if and only if c = 0 ∧ δ = (pw -b)/c, as we know from bad 2

  is corrupted before Step 2. In this case, Sim CO only needs to simulate H before S becomes corrupted (afterwards, both parties are corrupt and there is nothing to simulate). When R sends U in Step 2, Sim CO learns u, v s.t. U = g u A v . Sim CO now proceeds to simulate H exactly as in the case where S is corrupted before Step 1, except that it aborts if it ever sets both k 0 , k 1 = ⊥. As in the case where the Sender is corrupted before Step 1, Sim CO 's simulation is indeed efficient, since it knows y and can hence check the necessary relations in the exponent of U.

  2

  •(-b) ) for b ∈ {0, 1}, (i.e., it checks with respect to both b = 0 and b = 1). If any queries have been made before U was set by the corrupted R, Sim CO also checks whether they have this format. * If not, it samples k ← {0, 1} κ and returns k. * If Sim CO has previously set e b = ⊥ (see below) it sets k b := e b ⊕ m b . If m b has not been output to Sim CO as described above, Sim CO aborts. * Else (i.e., e b was not previously set), it sets k b ← {0, 1} κ and returns k b .In Step 3, Sim CO samples e 0 , e 1 ← {0, 1} κ and sends them to R. After Sim CO performs Step 3 of the protocol, Sim CO inputs (deliver, sid , S) to F OT which prompts the output (output, sid ) to S. Once S is corrupted (after Step 3), Sim CO learns m 0 , m 1 . It outputs (y, m 0 , m 1 ) to E.-R is corrupted between Step 2 and Step 4. In this case, the simulation for R can be carried out as in the case where S is corrupted before Step 1. In addition, after S performs Step 3 of the protocol, Sim CO inputs (receive, sid , b), (deliver, sid , S) to F OT (in this order). This prompts the output (output, sid ) to S, since S is honest at this point and thus has input (send, sid , m 0 , m 1 ) to F OT . Moreover, Sim CO aborts upon setting both k 0 , k 1 = ⊥. -R is corrupted after Step 4. Same as previous case, except that Sim CO does not have to abort if R is corrupted after S.

One can consider formalizing the AGM within the UC framework by introducing a functionality F AGM that "forces" arbitrary algorithms to behave algebraically by registering group elements and their representations in a central repository. This has a number of disadvantages that we discuss in Appendix A. Our approach is closer to the spirit of the AGM, which idealizes groups by quantifying over restricted classes of adversaries.

For a review of the security proofs available for both protocols at the time, see https://mailarchive.ietf.org/ arch/msg/cfrg/47pnOSsrVS8uozXbAuM-alEk0-s.

Formally, we assume an encoding of group elements that distinguishes them from arbitrary strings. This can be done by simply prefixing any group element with a 0 and any other string (not necessarily representing a group element) with a 1. Following prior work[START_REF] Fuchsbauer | The algebraic group model and its applications[END_REF], we use bold capital letters to denote group elements (except for the generator g).

Formally, we consider protocols having access to a FCRS functionality, where FCRS runs a group-generation algorithm to obtain G (and possibly additional group elements), and then sends G (and any other elements) to parties that request it. Note that the protocol may use other groups, but we only require the adversary to be algebraic with respect to G.

Note that this Sπ is an imaginary machine supposed to run inside S, whereas the "actual" Sπ is the simulator in the execution of φ. Same with step 3 below.

This step could be replaced with a search for a consistent entry using a DDH oracle to the fixed basis A, resulting in a tighter reduction to Strong SqDH where the qH factor disappears.

As we will see, this determines the machines from which µ can receive messages.

Note that π may not contain such a machine. If not, then ID is called an external identity of µ . Intuitively this is some party outside the protocol (e.g., in some higher-level protocol) that calls µ .

Formally, an ITM has three externally writable tapes: an input tape, a subroutine-output tape, and a backdoor tape. The incoming message m is written on one of these tapes of µ (or E), depending on the label.

As we can see, the environment E essentially covers all external identities of π. It might look odd that we let the main machines communicate with some external identities, rather than with E directly. This is for the sake of composibility: in the case that π is a sub-protocol of some higher-level protocol ρ π , we need π's main machines to communicate with machines in ρ := ρ π \ π, which has the corresponding external identity. If we only allowed π's main machines to communicate with identity 0 (i.e., the environment), then they would not be able to communicate with their "callers" in ρ, and thus composibility could not be well-defined.

Formally, these rules are enforced via a control function, which on input an execution up-to-date, outputs a bit indicating allow/disallow. If the output is 1 then the message is delivered; otherwise the environment is activated. The control function has similar effects to those of the communication sets in the simplified model.

Note that this adversary is not A: both this adversary and ED are machines in protocol execution (of π or φ), whereas ED runs A as a subroutine. In other words, from ED's point of view, this adversary is "external," whereas A is "internal."

This step could be replaced with a search for a consistent entry using a DDH oracle to the fixed basis A, resulting in a tighter reduction to Strong SqDH where the qH factor disappears.

Simulator S for SPAKE2 proc Initialize( ) Get CRS=(M, N)

On input (NewSession, sid, P, P , role) from F pwKE If ¬(π sid P =⊥) discard input. If role = init x ← ← Zq; X ← M x ; π sid P ← (x, (P, P , sid , X , ⊥), ⊥, init) Send SendInit(P, P , sid , X ) to E Else y ← ← Zq; Y ← N y ; π sid P ← (y, (P , P, sid , ⊥, Y ), ⊥, resp)

On message SendInit(P, P , sid , (X , alg)) from E Ignore if π sid P = (y, (P, P , sid , ⊥, Y ), ⊥, resp) (A unique π sid P satisfies the above check for some y and Y ) K ← ← K (Can't interrupt passive sessions so F sets =K at output) If π sid P = ( • , (P, P , sid , X , ⊥), ⊥, init) Jump to Complete (First check whether X was constructed as per protocol) If alg = [(g, x); (M, pw)] Query (TestPwd, sid, P , pw) to F pwKE If F pwKE responds with "correct guess" Y ← Y / N pw ; K ← H(P, P , sid , X , Y , pw, Y x ) (Interrupt all other sessions so independent key is set) Else Query (TestPwd, sid , P , ⊥) to F pwKE Complete: Send SendResp(P , P, sid , Y ) to E π sid P ← (y, (P, P , sid , X , Y ), K, resp) Query (NewKey, sid, P , K) to F pwKE On message SendResp(P , P, sid , (Y , alg)) from E Ignore if π sid P = (x, (P, P , sid , X , ⊥), ⊥, init) (A unique π sid P satisfies the above check for some x and X ) K ← ← K (Can't interrupt passive sessions so F sets =K at output) If π sid P = ( • , (P, P , sid , X , Y ), • , resp) Jump to Complete (First check whether Y was constructed as per protocol)

Query (TestPwd, sid , P, pw) to F pwKE If F pwKE responds with "correct guess" X ← X / M pw ; K ← H(P, P , sid , X , Y , pw, X y ) (Interrupt all other sessions so independent key is set) Else Query (TestPwd, sid , P, ⊥) to F pwKE Complete: π sid P ← (x, (P, P , sid , X , Y ), K, init) Query (NewKey, sid, P, K) to F pwKE Simulator S for CPace proc H1(sid , P, P , pw) (non-repeat queries) r ← ← Zq; G ← g r ; T1[sid , P, P , pw] ← G; return G Simulator aborts if at any point T1 is non-injective.

On input (NewSession, sid, P, P , role) from On input (NewSession, sid , P, P , pw, role) from E At most one instance for a given sid at P .

On message SendInit(P, P , sid , X ) from E via D Ignore if π sid P = (y, (P, P , sid, ⊥, Y ), ⊥, pw, resp) (A unique π sid P satisfies the above check)

On input (NewSession, sid, P, P , role) from

If ∃π sid P = ( • , (P, P , sid , (X , alg), Y ), • , resp) for which F pwKE holds pw:

Terminate outputting (Z/A αδ(y-pw) ) 1 δ(y-pw)(b+δc-pw) Fig. 11. Reduction B2 computes SqDH(A). T is initially empty. B2 runs F pwKE internally, so it can check password guesses and answer corrupt queries as in the ideal world. It can also check whether random oracle entries are consistent with the session passwords on termination.

On input (NewSession, sid, P, P , pw, role) from E At most one instance for a given sid at P . If role = init G ← H1(sid , P, P , pw) x ← ← Zq; X ← G x π sid P ← (x, (P, P , sid, X, ⊥), ⊥, init) Send SendInit(P, P , sid, X) to D Else G ← H1(sid , P , P, pw) y ← ← Zq; Y ← G y π sid P ← (y, (P , P, sid, ⊥, Y), ⊥, resp)

On message SendInit(P, P , sid, X = 1) from E via D Ignore if π sid P = (y, (P, P , sid, ⊥, Y), ⊥, resp) (A unique π sid P satisfies the above check) K ← H2(sid , X, Y, X y ) Send SendResp(P , P, sid , Y) to D π sid P ← (⊥, (P, P , sid, X, Y), K, resp) Output K On message SendResp(P , P, sid , Y = 1) from E via D Ignore if π sid P = (x, (P, P , sid, X, ⊥), ⊥, init) (A unique π sid P satisfies the above check) K ← H2(sid, X, Y, Y x ) π sid P ← (⊥, (P, P , sid, X, Y), K, init) Output K Simulator S proc H1(sid , P, P , pw) (non-repeat queries) r ← ← Zq; G ← g r ; T1[sid , P, P , pw] ← G; return G Simulator aborts if at any point T1 is non-injective.

On input (NewSession, sid, P, P , role) from

On message SendInit(P, P , sid , (X, alg) = 1) from E via D Ignore if π sid P = (ŷ, (P, P , sid , ⊥, Y), ⊥, resp) (A unique π sid P satisfies the above check) K ← ← K (Can't interrupt passive sessions so F sets =K at output) If π sid P = ( • , (P, P , sid , X, ⊥), ⊥, init) Jump to Complete (First check whether X was constructed as per protocol)

Query (TestPwd, sid, P , pw) to F pwKE If F pwKE responds with "correct guess" K ← H2(sid , X, Y, Y x ) (Interrupt all other non-passive sessions.) Else Query (TestPwd, sid , P , ⊥) to F pwKE Complete: Send SendResp(P , P, sid , Y) to D π sid P ← (⊥, (P, P , sid , X, Y), K, resp) Query (NewKey, sid, P , K) to F pwKE On message SendResp(P , P, sid , (Y, alg) = 1) from E via D Ignore if π sid P = (x, (P, P , sid , X, ⊥), ⊥, init) (A unique π sid P satisfies the above check) K ← ← K (Can't interrupt passive sessions so F sets =K at output) If π sid P = ( • , (P, P , sid , X, Y), • , resp) Jump to Complete (First check whether Y was constructed as per protocol) If alg = [(G, y)] ∧ (sid , P, P , pw, G) ∈ T1 Query (TestPwd, sid , P, pw) to F pwKE If F pwKE responds with "correct guess" K ← H2(sid, X, Y, X y ) (Interrupt all other non-passive sessions.) Else Query (TestPwd, sid , P, ⊥) to F pwKE Complete: π sid P ← (⊥, (P, P , sid , X, Y), K, init) Query (NewKey, sid, P, K) to F pwKE The simulator needs to observe adversarial random oracle queries on H1 but not on H2, and it does not need to program either of the random oracles. T1 is initially empty. proc H1(sid , P, P , pw)

Compute (TestPwd, sid , P , pw) as F pwKE If F pwKE responds with "correct guess" Then K ← H2(sid , X, Y, Y x ) Else Compute (TestPwd, sid , P , ⊥) as F pwKE Complete: Send SendResp(P , P, sid , Y) to D π sid P ← (ŷ, (P, P , sid , (X, alg), Y), K, resp) Compute (NewKey, sid , P , K) as