Forward Secrecy of SPAKE2

Abstract

Currently, the Simple Password-Based Encrypted Key Exchange (SPAKE2) protocol of Abdalla and Pointcheval (CT-RSA 2005) is being considered by the IETF for standardization and integration in TLS 1.3. Although it has been proven secure in the Find-then-Guess model of Bellare, Pointcheval and Rogaway (EUROCRYPT 2000), whether it satisfies some notion of forward secrecy remains an open question.

In this work, we prove that the SPAKE2 protocol satisfies the so-called weak forward secrecy introduced by Krawczyk (CRYPTO 2005). Furthermore, we demonstrate that the incorporation of key-confirmation codes in SPAKE2 results in a protocol that provably satisfies the stronger notion of perfect forward secrecy. As forward secrecy is an explicit requirement for cipher suites supported in the TLS handshake, we believe this work could fill the gap in the literature and facilitate the adoption of SPAKE2 in the recently approved TLS 1.3.

1 Introduction

1.1 SPAKE2 Protocol

Password Authenticated Key Exchange (PAKE) protocols allow two users, who only share a password, to agree on a high-entropy session key over a hostile network. The goal is to use the established session key to build a secure channel between the involved parties. The nature of passwords makes PAKEs vulnerable to on-line dictionary attacks, where an adversary tries to impersonate a user by guessing his password, engaging in a protocol execution and verifying if its guess was correct. An offline dictionary attack occurs when the protocol execution allows an adversary to launch an exhaustive offline search of the password. The intuition of security requires PAKEs to be vulnerable to online dictionary attacks only. The seminal work in this area is the Encrypted Key Exchange (EKE) protocol of Bellovin and Merritt [1]. Since then, various PAKE protocols have been proposed: PPK and PAK [2, 3], J-PAKE [4, 5], SRP [6], SPEKE [7] and SPAKE2 [8]. In parallel, prominent complexity-theoric security models for PAKEs have been proposed to get assurance on the claimed security properties by performing a rigorous analysis of the protocol in question [2, 9,10,11,12].

The SPAKE2 protocol, proposed by Abdalla and Pointcheval [8], is a one-round PAKE protocol proven secure in the Find-then-Guess (FtG) model of Bellare et al. [9] without considering forward secrecy. It is a simple, yet efficient protocol that, in addition to the pre-shared password, requires the protocol participants to share two Common Reference Strings (CRS) prior to the execution of the protocol. The adoption of the CRS yields to an elegant construction that does not require full domain hash functions, which are hard to implement efficiently in practice. On the other side, the CRS requires extra security assumptions that might be easy to satisfy in some scenarios but may be very restrictive in others [13]. Also, as it is a one-round protocol, only implicit authentication can be satisfied. Fortunately, the incorporation of key-confirmation codes allows the protocol participants to explicitly authenticate each other [14] and [15, Chap. 40].

Recently, the Internet Engineering Task Force (IEFT) community has revisited the deployment of SPAKE2 protocol: (i) as stand alone specification [16], (ii) its usage as pre-authentication mechanism in Kerberos protocol [17] and (iii) its adoption in TLS 1.3 protocol, specifically in the handshake when pre-shared keys for authentication are available [18, 19]. The discussion of forward secrecy in SPAKE2 has been a common factor in the aforementioned Internet Drafts.

1.2 PAKEs Adoption in TLS

Nowadays, the Transport Layer Security (TLS) is the de-facto standard to protect internet communications. It consists of two stages: the Handshake protocol where two parties agree on a session key, and the Record protocol where the communication is protected using the previously negotiated keys. Most of the TLS implementations provide only unilateral authentication, where client C authenticates server S during the handshake by means of public-key infrastructure (PKI), therefore identity disclosure of client to server is usually not supported.

While the unilateral server-authenticated approach might be sufficient for scenarios like internet surfing, it is certainly inadequate for real-world applications including email access, internet banking and social media, where client C needs to authenticate to server S to gain access to resources in S. In practice, the common approach for authenticating the client asks the client to send his user/password protected through a server-authenticated TLS channel. This approach protects the password against eavesdroppers but not against phishing attacks: An adversary can clone a legitimate website and fool the client to visit the fake website where he input his credentials. To make things worse, the adversary can manage to obtain a valid public-key certificate from a certification authority (CA) for his illegitimate web page. Indeed, the client may see on his web browser “secure connection” as a TLS connection may be established between the client and the cloned website controlled by the adversary.¹

Fortunately, PAKEs stand as a strong candidate for scenarios where two parties require to mutually authenticate each other while intrinsically protecting their shared password. In fact, the Secure Remote Password (SRP) protocol [6] has been incorporated in previous versions of TLS and standardized in the form of RFC5054 [20]. Specifically, the SRP protocol was made available as cipher suite in the TLS handshake. Similarly, the IETF is currently considering the adoption of SPAKE2 in TLS 1.3 handshake [18], in particular in the TLS handshake, for scenarios where authentication is made using pre-shared password available between the Client and Server.

In the recently approved TLS 1.3, it has explicitly been a design goal to provide forward secrecy for the session keys used to construct the TLS channel. In particular, static RSA and Diffie-Hellman cipher suites were removed to favor public-key based key-exchange mechanism that guarantee forward secrecy. Therefore, formally proving that SPAKE2 satisfies some significant notion of forward secrecy would increase its possibilities of acceptance into TLS 1.3.

Remark: While PAKEs adoption in web authentication is a good approach to protect user’s password during the authentication phase, there are still usability concerns that slow down the implementation of PAKEs in TLS to properly prevent phishing attacks. This implementation requires an easy to identify “safe area” available in the web browser where the passwords should be entered [21].

1.3 Forward Secrecy

Forward secrecy is a desirable property which has been explicitly a design goal in relevant AKE and PAKE protocols [3, 4, 22, 23], and more recently in TLS 1.3 [19].² Roughly speaking, it ensures the protection of session keys even if the long-term secret of the participants gets later compromised [24]. For instance: (i) the password file at the server could be leaked or (ii) via phishing attacks a client could reveal his password to some malicious entity.

The notion of forward secrecy appeared first in [24] and was later formalized in [23, 25,26,27] for AKE and in [9, 28] for PAKE protocols. We distinguish weak forward secrecy (wFS) from perfect forward secrecy (PFS): The former protects session keys after compromise of long-term key material, but only those sessions created without the active participation of the attacker [23], while the latter protects all session keys which were negotiated before corruption, i.e. even those created with the active intervention of the adversary. It is generally accepted that PFS is difficult to satisfy in protocols which only guarantee implicit authentication. For instance, Krawczyk [23] states that PFS cannot be satisfied by two-flow protocols using public-key as authentication mechanism. Therefore Krawczyk proposed the notion of weak Forward Secrecy (wFS) as an attempt to satisfy some notion of security when long-term material is compromised but only for those sessions without the active participation of the adversary.

PFS and Key-Confirmation: The authors in [3, 9, 25] demonstrated that PFS can be satisfied when explicit authentication is added to protocols that initially satisfy only wFS. The idea is the following: Suppose P is a 2-flow PAKE protocol satisfying only implicit authentication. The adversary sends the first message to Bob masquerading as Alice, Bob computes the session key, sends back the second message and finishes his protocol execution. Then the adversary waits for the leakage of the long-term key and that could possibly help her to compute the same session key as Bob. For this scenario, the notion of PFS requires the adversary not to learn Bob’s session key, which can be easily avoided by requiring key-confirmation, since then Bob will not accept the session key before he authenticates his communication partner.

1.4 Our Contribution

We propose a new version of SPAKE2 which we name PFS-SPAKE2. This is essentially SPAKE2 but with key-confirmation codes incorporated into the protocol. This well known approach allowed us to meet the PFS requirement in a provably secure way even in the case of active adversaries, making it a suitable candidate for standardization and adoption in the TLS 1.3 protocol. In addition, we prove that the original SPAKE2 satisfies weak forward secrecy.

2 Security Model with Forward Secrecy

Notation. We use calligraphic letters to denote adversaries, typically $\mathcal {A}$ and $\mathcal {B}$. We write $s \xleftarrow {\$} S$ for sampling uniformly at random from set S and |S| to denote its cardinality. The output of a probabilistic algorithm A on input x is denoted by $y \leftarrow A(x)$, while $y:=F(x)$ denotes a deterministic assignment of F(x) to the variable y. Let $\{0,1\}^*$ denote the bit string of arbitrary length while $\{0,1\}^l$ stands for those of length l. Let $\lambda$ be the security parameter, $negl(\lambda )$ denote a negligible function and PPT stand for probabilistic polynomial time.

Next we describe the well-known security model of Bellare, Pointcheval and Rogaway [9], which we use to prove the security of PFS-SPAKE2 and SPAKE2 protocol. Frequently referred as the Find-then-Guess (FtG) model, it is an extension of [29, 30] to the password setting. We assume the reader is familiar with the model.

PAKE PROTOCOL. A PAKE protocol is defined by a pair of algorithms ($Gen, \mathcal {P}$). Gen is the password generation algorithm. It takes as input the dictionary $D$, a probability distribution $\mathcal {Q}$ and initializes the protocol participants with some password. The protocol description $\mathcal {P}$ defines how honest participants behave.

PROTOCOL PARTICIPANTS. Each participant is either a client $C \in \mathcal {C}$ or a server $S \in \mathcal {S}$. Let $\mathcal {U} = \mathcal {C} \cup \mathcal {S}$ denote the set of all (honest) users and $\mathcal {C} \cap \mathcal {S} = \varnothing$.

LONG-TERM SECRETS. Each client C holds a password $\pi _C$ and server S holds a vector of passwords for all clients i.e. $\pi _S = <\pi _C>_{C\in \mathcal {C}}$ s.t. for each client C $\pi _S[C] = \pi _C$. We consider the client-server scenario where there is a single server S. The passwords are assumed to be independent and uniformly distributed.

PROTOCOL EXECUTION. $\mathcal {P}$ is a probabilistic algorithm that defines how users respond to signals from the environment. We assume the presence of a PPT adversary $\mathcal {A}$ with full control of the network and an unlimited number of user instances. Specifically, let $\varPi _{U}^{i}$ denote the instance i-th of user $U \in \mathcal {U}$. In cases where distinction matters, let $\varPi _{C}^{i}$ and $\varPi _{S}^{j}$ denote the i-th and j-th instance of client $C \in \mathcal {C}$ and server S respectively.

Security is defined via a game played between the challenger $\mathcal {CH}$ and adversary $\mathcal {A}$ whose goal is to break the semantic security of the established session keys. $\mathcal {A}$ controls the oracle user instances with the following queries:

• Send(U, i, m): A message m is sent to instance $\varPi _{U}^{i}$ and processed according to the protocol description $\mathcal {P}$. Its output is given to $\mathcal {A}$.

• Execute(C, i, S, j): This query causes an honest run of protocol $\mathcal {P}$ between $\varPi _{C}^{i}$ and $\varPi _{S}^{j}$, the transcript of execution is given to $\mathcal {A}$.

• Reveal(U, i): The session key $sk_U^i$ held at $\varPi _{U}^{i}$ is given to $\mathcal {A}$. It requires the $sk_U^i$ to be already computed, i.e. $\varPi _{U}^{i}$ must be on terminate state.

• Corrupt(U). The adversary obtains the password of user U. If $U=C \in \mathcal {C}$, then $\mathcal {A}$ receives $\pi _C$, else if $U=S$, then $\mathcal {A}$ receives $\pi _S = <\pi _C>_{C\in \mathcal {C}}$.

• Test(U, i): $\mathcal {CH}$ flips a bit b and answers the query as follows: if $b=1$ $\mathcal {A}$ gets the session key $sk_U^i$, otherwise she receives $r \xleftarrow {\$} \{0,1\}^{\kappa }$, where $\{0,1\}^{\kappa }$ denotes the length of the session key space.

2.1 Definitions

Partnering. Two instances, $\varPi _{C}^{i}$ and $\varPi _{S}^{j}$, are partnered if both accept, holding ($sk_C^i, sid_C^i, pid_C^i$) and ($sk_S^j, sid_S^j, pid_S^j$) respectively and also:

• 1. $sk_C^i = sk_S^j$, $sid_C^i = sid_S^j$, $pid_C^i = S$, $pid_S^j = C$ and

• 2. no other instance accepts with the same session identifier sid, except with negligible probability.

The notion of freshness avoids scenarios where an adversary could trivially win the security experiment. Next we define two notions of freshness depending on the desired of forward secrecy guarantee: The first flavour models PFS, where the intuition is to consider as legitimate targets of a Test query those instances which session keys were negotiated before the corruption of any principal. The second variant models wFS, which does not guarantee the secrecy of those sessions keys which were negotiated with the active intervention of an adversary (determined via partnering) whenever some user has been corrupted.

PFS-Freshness. An instance $\varPi _{U}^{i}$ is PFS-fresh unless:

• A Reveal query was made to $\varPi _{U}^{i}$ or its partner or

• There was a Corrupt(U’) and a Send(U, i, m) query, $\varPi _{U}^{i}$ does not have a partner and the corruption of any user $U'$ occurs before the Test query.

wFS-Freshness. An instance $\varPi _{U}^{i}$ is wFS-fresh unless:

• A Reveal query was made to $\varPi _{U}^{i}$ or its partner or

• There was a Corrupt($U'$) and a Send(U, i, m) query, $\varPi _{U}^{i}$ does not have a partner and the corruption of any user $U'$ occurs at any time.

Advantage of the Adversary. Let $\mathrm {Succ}^{\mathrm {PFS}\text {-}\mathrm {FtG}}_P$ be the event where $\mathcal {A}$ asks a single Test query directed to a PFS-fresh instance that has terminated, $\mathcal {A}$ outputs his guess $b'$ and wins i.e. $b'=b$. The advantage of $\mathcal {A}$ attacking protocol P is:

$$\begin{aligned} \mathrm {Adv}^{\mathrm {PFS}\text {-}\mathrm {FtG}}_P(\mathcal {A}) = 2 \cdot {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_P (\mathcal {A})}\,\right] } -1 \end{aligned}$$

(1)

Definition 1

(PFS-FtG security). Protocol P is FtG secure and satisfies perfect forward secrecy if for all PPT adversaries there exists a negligible function $\epsilon (\cdot )$ such that:

$$ \mathrm {Adv}^{\mathrm {PFS}\text {-}\mathrm {FtG}}_{P} (\mathcal {A}) \le n_{se}/|D| + \epsilon (\lambda ), $$

where $n_{se}$ is the number of Send queries and $D$ is the password dictionary.

We similarly define FtG security with weak forward secrecy, the only change is in the advantage function, where the Test query must be made to a wFS-fresh instance. From inspection, it is easy to see that PFS-FtG $\rightarrow$ wFS-FtG security.

2.2 Cryptographic Hardness Assumptions

Let $\mathbb {G}$ be a multiplicative a group, with generator g and $|\mathbb {G}| = q$. For $X = g^x$ and $Y=g^y$, let DH$(X,Y) = g^{xy}$, where $\{g^x, g^y, g^{xy}\} \in \mathbb {G}$.

Definition 2

(Computational Diffie-Hellman (CDH) Problem). Given $(g, g^x, g^y)$ compute $g^{xy}$, where $\{g^x, g^y, g^{xy}\} \in \mathbb {G}$ and $(x,y) \xleftarrow {\$} \mathbb {Z}_q^2$. Let the advantage of an algorithm $\mathcal {A}$ in solving the CDH problem be:

$$ \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\mathcal {B}) = \Pr {[(x,y) \xleftarrow {\$} \mathbb {Z}_q^2,X=g^x, Y=g^y: \mathcal {B}(X,Y) = \text {DH}(X,Y)]}. $$

Under the CDH assumption there exist sequences of cyclic groups $\mathbb {G}$ indexed by $\lambda$ s.t. $\forall \mathcal {B}$ running in time t polynomial in $\lambda$, $\mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\mathcal {B})$ is a negligible function.

3 PFS-SPAKE2

Inspired by MacKenzie’s work [3], we propose to incorporate key-confirmation codes into the SPAKE2 protocol [8] to achieve PFS in a provably secure manner.

3.1 Protocol Description

In Fig. 1 we provide the technical description of the proposed PFS-SPAKE2 protocol. Before the protocol is executed, public parameters must be chosen and published. These parameters include the description of group $\mathbb {G}$, hash functions $H_1$, $H_2$, $H_3$ and a CRS M – which we require to be choosen at random from $\mathbb {G}$ and its discrete logarithm to be kept secret. These constraints on the CRS can be achieved either by having a third trusted party or by assuming a public source of randomness to publicly derive M. Our protocol is instantiated over group $\mathbb {G}$, a q order subgroup of $\mathbb {Z}_p^*$ where CDH assumption holds and p, q are safe prime numbers. The protocol requires that passwords are encoded in $\mathbb {Z}_q$.

Fig. 1.

PFS-SPAKE2 protocol.

Comparison to Existing PAKEs. The efficiency of a PAKE protocol is defined by (i) the number of communication rounds until the protocol terminates, (ii) the total number messages exchanged and (iii) the computational cost of the protocol. Compared to the original SPAKE2, the proposed PFS-SPAKE2 protocol benefits from explicit authentication and strong security guarantees for PFS. It is also slightly less computationally expensive, as it requires the client to compute only three exponentiations instead of four, i.e. no need to compute $N^{\pi } \in \mathbb {G}$. These improvements usually come at the cost of increasing the number of rounds and message flows and unfortunately our protocol is not an exception [3, 23].

In Table 1 we summarize the comparison of PFS-SPAKE2 with other relevant PAKE protocols with full security proofs.³ Notably J-PAKE satisfies PFS and requires only two communication rounds; however, it is computationally more expensive than PFS-SPAKE2 as the former requires 28 exponentiations while the latter only 5. Furthermore, J-PAKE with key-confirmation requires the same number of communication rounds as PFS-SPAKE2. Alternatively, PAK and PFS-SPAKE2 are similar in terms of efficiency, PFS and key confirmation guarantees, yet the usage of CRS in the latter allowed us to achieve tighter security reductions to the CDH assumption than the original results for PAK [3, 31].

Table 1. Comparison with existing PAKEs for Client-Server scenarios.

3.2 Security of PFS-SPAKE2

Theorem 1

(Security in the PFS-FtG Model). Let P be the protocol specified in Fig. 1, instantiated in group $\mathbb {G}$ and with passwords uniformly distributed over dictionary $D$. Let $\mathcal {A}$ be an adversary that runs in time t polynomial in $\lambda$, makes at most $n_{ex}$, $n_{se}$, $n_{ro}$ queries of type execute, send and random oracle. Then:

$$\begin{aligned} \small \mathrm {Adv}^{\mathrm {PFS}\text {-}\mathrm {FtG}}_P(\mathcal {A}) \le \frac{n_{se}}{|D|} + \mathcal {O} \left( \frac{(n_{se} + n_{ex})(n_{se} + n_{ex} + n_{ro})}{q} + \right. \\ \left. n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}({\mathcal {B}^{\mathcal {A}}}) + n_{se} n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\tilde{\mathcal {B}}^{\mathcal {A}}) +n^2_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\hat{\mathcal {B}}^{\mathcal {A}}) \right) , \end{aligned}$$

where $\mathcal {B}^{\mathcal {A}}$, $\tilde{\mathcal {B}}^{\mathcal {A}}$ and $\hat{\mathcal {B}}^{\mathcal {A}}$ are CDH-solver algorithms running in time $t' = \mathcal {O} ( t + (n_{se} + n_{ex} + n_{ro})\cdot t_{exp} )$, where $t_{exp}$ is the time for an exponentiation in $\mathbb {G}$.

To prove the security of PFS-SPAKE2, we introduce a sequence of protocols $\mathrm {P_0 \ldots P_7}$, where $\mathrm {P_0}$ is the original protocol and $\mathrm {P_7}$ allows only online dictionary attacks. Let $\mathrm {G_i}$ be the security game associated to $\mathrm {P_i}$. We borrow from [3] the structure and the nomenclature to prove the security of our PFS-SPAKE2 protocol and refer to Appendix A for the necessary terminology.

The security proof requires the random oracle model: each new random oracle query $H_l$ for $l \in \{1,2,3\}$ is answered with a fresh random output, however, if the query has been previously made, it is answered consistenly with previous queries. In cases where it is clear enough, we write $H_l(\cdot )$ to refer to query of the form $H_l(C,S,X^*,Y,\sigma ,\pi )$. For easiness of the proof we assume that for each $H_l(C,S,X^*,Y,\sigma ,\pi )$ query made by $\mathcal {A}$, with $l \in \{1,2,3\}$, the corresponding $H_{l'}(\cdot )$ and $H_{l''}(\cdot )$ are also made, with $l',l'' \in \{1,2,3\} \backslash \{l\}$ and $l'\ne l''$. The simulator sets $M:= g^m \in \mathbb {G}$, where $m \xleftarrow {\$} \mathbb {Z}_q$.

In the following games, we simply write $\mathrm {Succ}^\mathrm {FtG}_{P_i}$ instead of $\mathrm {Succ}^{\mathrm {PFS}\text {-}\mathrm {FtG}}_{P_i}$ to denote the success probability of $\mathcal {A}$ winning in game $\mathrm {G_i}$.

• Game ${\mathbf {{G}_0}}$ : Execution of original protocol.

• Game ${\mathbf {{G}_1}}$ : Uniqueness of honest sessions.

During the interaction with adversary $\mathcal {A}$, the challenger needs to simulate honest instances and generate the $X^*$ and Y terms according to the protocol description. Let $F_1$ be the event where there is a collision between either an $X^*$ or Y value, with previously seen $X^*$ or Y values. If $F_1$ occurs, the challenger draws random values again until he arrives at a $X^*$ or Y term that has not been previously seen. It is easy to show that the probability of $F_1$ occurring is bounded by the birthday paradox. Then for all $\mathcal {A}$:

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_0}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_1}(\mathcal {A})}\,\right] } + \mathcal {O} \left( \frac{(n_{se} + n_{ex})(n_{se} + n_{ex} + n_{ro})}{q} \right) . \end{aligned}$$

Game $\mathbf {{G}_2}$: Prevent Lucky Guesses on Hash Outputs.

This game forces $\mathcal {A}$ to query the random oracle whenever she needs to compute any hash $H(\cdot )_l$. As a result, this game rules out the possibility of $\mathcal {A}$ to output correct values $k,k'$ or sk without calling the corresponding random oracle.

Let $\mathrm {P_2}$ be a protocol identical to $\mathrm {P_1}$, except that honest instances respond to Send and Execute queries without making any random oracle queries and subsequent random oracle queries made by $\mathcal {A}$ are backpatched to be consistent with previous queries. Next we detail the changes in $\mathrm {P_2}$.

• In an Execute(C, i, S, j) query set $X^* = g^{\tau [C,i]}$ and $Y = g^{\tau [S,j]}$, where $\tau [\cdot ] \xleftarrow {\$} \mathbb {Z}_q$, $k, k' \xleftarrow {\$} \{0,1\}^\kappa$ and $sk_S^j \leftarrow sk_C^i \xleftarrow {\$} \{0,1\}^\kappa$, where $\{0,1\}^\kappa$ denotes the session key space.

• In a CLIENT ACTION 0 query to $\varPi _{C}^{i}$, set $X^* = g^{\tau [C,i]}$, where $\tau [C,i] \xleftarrow {\$} \mathbb {Z}_q$.

• In a SERVER ACTION 1 query to $\varPi _{S}^{j}$, set $Y = g^{\tau [S,j]}$ and $k \xleftarrow {\$} \{0,1\}^\kappa$, where $\tau [S,j] \xleftarrow {\$} \mathbb {Z}_q$.

• In a CLIENT ACTION 1 query to $\varPi _{C}^{i}$ proceed as follows:

  • If $\varPi _{C}^{i}$ is paired with $\varPi _{S}^{j}$ then set $k',sk_C^i \xleftarrow {\$} \{0,1\}^\kappa$.

  • Else if this query triggers a testpw($C,i,S,\pi _c,l$) event, for some $l\in \{1,2,3\}$, then set $k'$ and $sk_C^i$ to the associated value of the event testpw ($C,i,S,\pi _c,2$) and testpw($C,i,S,\pi _c,3$) respectively.

  • Else $\varPi _{C}^{i}$ aborts.

• In a SERVER ACTION 2 query to $\varPi _{S}^{j}$ proceed as follows:

  • If $\varPi _{S}^{j}$ is paired with $\varPi _{C}^{i}$ after some CLIENT ACTION 1 query to $\varPi _{C}^{i}$, then set $sk_S^j \leftarrow sk_C^i$.

  • Else this query triggers a testpw($S,j,C,\pi _c,l$), with $l \in \{ 1,2,3\}$, set $sk_S^j$ to the associated value of the event testpw($S,j,C,\pi _c,3$).

  • Else instance $\varPi _{S}^{j}$ aborts.

• In an $H_l(C,S,X^*,Y,\sigma ,\pi )$ query made by $\mathcal {A}$, if it triggers a testpw($C,i,S,\pi _C,l$), testpw($S,j,C,\pi _C,l$) or testexecpw($C,i,S,j,\pi _C$) event, then output the associated event of the corresponding event. Otherwise output $v \xleftarrow {\$} \{0,1\}^\kappa$.

Claim 1

For all adversaries $\mathcal {A}$, ${\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_1}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_2}(\mathcal {A})}\,\right] } + \frac{n_{se}}{2^\kappa }$.

Proof

In SERVER ACTION 2 to $\varPi _{S}^{j}$, the input $k'$ determines whether the instance $\varPi _{S}^{j}$ should terminate or abort. Let $F_1$ be the event where in a SERVER ACTION 2 to $\varPi _{S}^{j}$, it terminates such that (i) $\varPi _{S}^{j}$ is not paired with $\varPi _{C}^{i}$ and (ii) testpw($S,j,C,\pi _C,l$) event does not occur, for $l \in \{1,2,3\}$, i.e. $\mathcal {A}$ luckily guessed the correct $k'$ value. Then ${\Pr \left[ \,{F_1}\,\right] } \le n_{se}/2^\kappa$.    $\square$

Game $\mathbf {{G}_3}$ : Do not backpatch $\varvec{H_l(\cdot )}$ queries against Execute queries.

This game shows that there is no need to backpatch $H_l(\cdot )$ queries to maintain consistent views against Execute queries. More formally, let $\mathrm {P_3}$ be identical to $\mathrm {P_2}$ except that, in a $H_l(C,S,X^*,Y,\sigma ,\pi _C)$ query made by $\mathcal {A}$, the simulator does not verify whether the testexec($C,i,S,j,\pi _C$) event occurs or not. Let $F_2$ and $F_3$ denote the testexec($C,i,S,j,\pi _C$) event occurring in $P_2$ and $P_3$ respectively.

Claim 2

For all adversaries $\mathcal {A}$, $|{\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_2}(\mathcal {A})}\,\right] } - {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_3}(\mathcal {A})}\,\right] }| \le {\Pr \left[ \,{F_2}\,\right] }$.

Proof

$\mathrm {P_2}$ and $\mathrm {P_3}$ are identical protocols until the testexec($C,i,S,j,\pi _C$) event occurs. The observation is that the events $F_2$ and $F_3$ are triggered as result of some interaction $\mathcal {CH}_2$ vs $\mathcal {A}$ and $\mathcal {CH}_3$ vs $\mathcal {A}$ respectively, however by definition they are identical. Then it follows that ${\Pr \left[ \,{F_2}\,\right] } = {\Pr \left[ \,{F_3}\,\right] }$ and to conclude the proof we simply apply Shoup’s Difference Lemma [33].    $\square$

Claim 3

Given $\mathcal {A}$, there exists a CDH-solver $\mathcal {B}^{\mathcal {A}}$ with running time $t' = \mathcal {O} ( t + (n_{se} + n_{ex} + n_{ro})\cdot t_{exp} )$ such that:

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_2}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_3}(\mathcal {A})}\,\right] } + n_{ro}\cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\mathcal {B}^{\mathcal {A}}), \end{aligned}$$

Proof

Let $\epsilon$ be the probability that testexec($C,i,S,j,\pi$) event occurs in $P_2$. We build an adversary $\mathcal {B}^{\mathcal {A}}$ whose goal is to solve the CDH problem using adversary $\mathcal {A}$ as a subroutine and with success probability $\epsilon /n_{ro}$. On input $(A=g^\alpha , B=g^\beta )$, $\mathcal {B}^{\mathcal {A}}$ simulates $P_2$ to $\mathcal {A}$ with the following changes:

• 1. For every Execute(C, i, S, j) query made by $\mathcal {A}$, the simulator $\mathcal {B}^{\mathcal {A}}$ sets $X^* = A \cdot g^{r_1}$, $Y = B \cdot g^{r_2}$, $k, k' \xleftarrow {\$} \{0,1\}^\kappa$ and $sk_S^j \leftarrow sk_C^i \xleftarrow {\$} \{0,1\}^\kappa$, where $r_1,r_2 \xleftarrow {\$} \mathbb {Z}_q$ are known to the simulator.

• 2. For every $H_l(C,S,X^*,Y, \sigma , \pi _C)$ query, where $l \in \{1,2,3\}$, $X^*$ and Y are generated via an Execute(C, i, S, j) query, add $\gamma$ to the set S-DH, where:

  $$\begin{aligned} \gamma = {\sigma \cdot B^{m\cdot \pi _C} \cdot M^{r_2 \cdot \pi _C}}/{B^{r_1} \cdot A^{r_2} \cdot g^{r_1 r_2}} \end{aligned}$$

• 3. When $\mathcal {A}$ finishes, the set S-DH contains at most $n_{ro}$ elements, where each item a possible solution to DH($g^\alpha , g^\beta$). Then $\mathcal {B}^{\mathcal {A}}$ outputs $\gamma \xleftarrow {\$}$ L-DH.

The adversary $\mathcal {A}$ can only distinguish $\mathrm {P_2}$ from $\mathrm {P_3}$ once testexec($C,i,S,j,\pi$) has occurred, but this happens with probability $\epsilon \le n_{ro}\cdot \mathrm {Adv}^\mathrm {CDH}_{G_q} (t')$. We make the observation that ${\mathrm {G}_3}$ guarantees forward secrecy for session keys established via Execute queries.    $\square$

Game $\mathbf {{G}_4}$ : Check for successful password guesses.

Let $\mathrm {P_4}$ be identical to $\mathrm {P_3}$, except that if correctpw event occurs, the protocol stops and the adversary automatically wins.

Claim 4

For all PPT adversaries $\mathcal {A}$, ${\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_3}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_4}(\mathcal {A})}\,\right] }$.

Proof

Obvious.    $\square$

This game simply counts for an adversary who is successful in an online dictionary attack by impersonating either a Client or the Server. The implication is that from $\mathrm {P_4}$, until either correctpw event or a Corrupt query occurs, no unpaired client or server instance will terminate.

Game $\mathbf {{G}_5}$ : Randomized session keys for paired instances.

Let $\mathrm {P_5}$ be identical to $\mathrm {P_4}$ except that if the pairedpwguess event occurs the protocol stops and the adversary fails.

In this game we will demonstrate that an adversary $\mathcal {A}$ who (i) may actively corrupt any Client or Server, i.e. $\mathcal {A}$ knows the corresponding correct password $\pi _C$ and (ii) manages to compute k, $k'$ or sk for paired instances $\varPi _{C}^{i}$ and $\varPi _{S}^{j}$, is also a CDH-solver. Let $F_4$ and $F_5$ denote the pairedpwguess event occurring in $\mathrm {P_4}$ and $\mathrm {P_5}$ respectively.

Claim 5

For all adversaries $\mathcal {A}$, $|{\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_4}(\mathcal {A})}\,\right] } - {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] }| \le {\Pr \left[ \,{F_4}\,\right] }$.

Proof

Identical to Claim 2.    $\square$

Claim 6

Given $\mathcal {A}$, there exists CDH-solver $\tilde{\mathcal {B}}^{\mathcal {A}}$ with running time $t' = \mathcal {O} ( t + (n_{se} + n_{ex} + n_{ro})\cdot t_{exp} )$ such that:

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_4}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] } + n_{se} \cdot n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\tilde{\mathcal {B}}^{\mathcal {A}}), \end{aligned}$$

Proof

Let $\epsilon$ be the probability of pairedpwguess event happening. We build $\mathcal {B}^{\mathcal {A}}$, a CDH-solver with success probability $\epsilon / (n_{se} \cdot n_{ro})$. On input $(A=g^\alpha , B=g^\beta )$, $\tilde{\mathcal {B}}^{\mathcal {A}}$ sets $M =g^m \in \mathbb {G}$ for $m \xleftarrow {\$} \mathbb {Z}_q$, chooses $d \in \{1...n_{se}\}$ at random – a session target of the Test query – and simulates $\mathrm {P_4}$ to $\mathcal {A}$ with the following changes:

• 1. In a CLIENT ACTION 0 query to $\varPi _{C}^{d}$ with input S, set $X^* \leftarrow A$, where $\varPi _{C}^{d}$ is the client instance that $\tilde{\mathcal {B}}^{\mathcal {A}}$ hopes it remains PFS-fresh.

• 2. In a SERVER ACTION 1 query to $\varPi _{S}^{j}$ with input $\langle C,m \rangle$, where there was previous a CLIENT ACTION 0 query to $\varPi _{C}^{d}$ with input S and output $\langle C,m \rangle$, set $Y = B \cdot g^{r_{S,j}}$, where $r_{S,j} \xleftarrow {\$} \mathbb {Z}_q$.

• 3. In a CLIENT ACTION 1 query to $\varPi _{C}^{d}$, if $\varPi _{C}^{d}$ is unpaired then it aborts an also $\tilde{\mathcal {B}}^{\mathcal {A}}$ stops the simulation.

• 4. In a SERVER ACTION 2 query to $\varPi _{S}^{j}$, if it was paired with $\varPi _{C}^{d}$ after its SERVER ACTION 1 but now is not paired, then $\varPi _{S}^{j}$ aborts. However, the simulation continues as the instance $\varPi _{C}^{d}$ may still be target of the Test query.

• 5. When $\mathcal {A}$ finishes, then for every $H_l(C,S,X^*,Y,\sigma , \pi _C)$, made by $\mathcal {A}$, with $l \in \{1,2,3\}$ and where (i) $X^*$ and Y were generated by $\varPi _{C}^{d}$ and $\varPi _{S}^{j}$ respectively, (ii) $\varPi _{S}^{j}$ was paired with $\varPi _{C}^{d}$ after its SERVER ACTION 1 and (iii) $\varPi _{C}^{d}$ was paired with $\varPi _{S}^{j}$, then add $\gamma$ to the set S-DH, where:

  $$\begin{aligned} \gamma = {\sigma \cdot B^{m\cdot \pi _C} \cdot M^{r_{S,j}\cdot \pi _C}}\cdot {A^{-r_{S,j}}} \end{aligned}$$

• 6. The set S-DH contains at most $n_{ro}$ elements, where each one is a possible solution to DH($g^{\alpha },g^{\beta }$). Then $\tilde{\mathcal {B}}^{\mathcal {A}}$ picks $\gamma \xleftarrow {\$}$ L-DH as its output.

In this reduction the simulator $\tilde{\mathcal {B}}^{\mathcal {A}}$ has to guess the client instance target of the Test query, say $\varPi _{C}^{d}$. The freshness requirement guarantees that a Corrupt query is only possible after the Test query, directed to $\varPi _{C}^{d}$ (or its partner), has been placed. Following the reductionist approach, we showed that the pairedpwguess event occurs at most with probability $\epsilon \le n_{se} \cdot n_{ro} \cdot \mathrm {Adv}^\mathrm {CDH}_{G_q} (\tilde{\mathcal {B}}^{\mathcal {A}})$.    $\square$

Game $\mathbf {{G}_6}$: Prevent testing more two passwords per server instance.

In ${\mathrm {P}_6}$ we restrict an adversary, who tries to masquerade as a client, from testing two passwords per session, say $\pi _1$ and $\pi _2$, in an online dictionary attack. Concretely, let $\mathrm {P_6}$ be identical to $\mathrm {P_5}$ except that if doublepwserver event occurs, the protocol stops and the adversary fails.

Let $F_5$ and $F_6$ denote the doublepwserver event occurring in $\mathrm {P_5}$ and $\mathrm {P_6}$ respectively. By definition it follows that $\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A}) \wedge \lnot F_5 \Leftrightarrow \mathrm {Succ}^\mathrm {FtG}_{P_6}(\mathcal {A}) \wedge \lnot F_6$.

Claim 7

For all adversaries $\mathcal {A}$, $|{\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] } - {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] }| \le {\Pr \left[ \,{F_6}\,\right] }$.

Proof

Identical to Claim 2.    $\square$

Claim 8

Given $\mathcal {A}$, there exists a CDH-solver $\hat{\mathcal {B}}^{\mathcal {A}}$ with running time $t' = \mathcal {O} ( t + (n_{se} + n_{ex} + n_{ro})\cdot t_{exp} )$ such that:

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_6}(\mathcal {A})}\,\right] } + n^2_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\hat{\mathcal {B}}^{\mathcal {A}}), \end{aligned}$$

Proof

We construct an algorithm $\hat{\mathcal {B}}^{\mathcal {A}}$ that solves the CDH problem probability $\epsilon /n^2_{ro}$, where $\epsilon$ is the probability of pairedpwguess event occurring. On input ($A= g^a, B=g^b$), $\hat{\mathcal {B}}^{\mathcal {A}}$ simulates $\mathrm {G_5}$ to $\mathcal {A}$ with the following changes:

• 1. Set $M := A$

• 2. In a SERVER ACTION 1 to $\varPi _{S}^{j}$ with input $\langle C, X^*\rangle$ set $Y\leftarrow B \cdot g^y$, where $y \xleftarrow {\$} \mathbb {Z}_q$, and sends back $\langle Y, k \rangle$. From $P_4$ it holds that no unpaired instances can terminate. Specifically, unpaired client and server instances abort in CLIENT ACTION 1 and SERVER ACTION 2 respectively.

• 3. When $\mathcal {A}$ terminates, for every pair of queries $H_l(C,S,X^*,Y, \sigma _1, \pi _1)$ and $H_l(C,S,X^*,Y, \sigma _2, \pi _2)$, where $\pi _1 \ne \pi _2$, add $\gamma$ to the S-DH, where:

  $$\begin{aligned} \gamma = {A^{-y}} \cdot \left( {\sigma _1}/{\sigma _2} \right) ^{(\pi _2 - \pi _1)} \end{aligned}$$

• 4. The set S-DH contains at most $(n_{ro})^2$ elements and each element in the set is a possible solution to DH(A, B). Then $\hat{\mathcal {B}}^{\mathcal {A}}$ outputs $\gamma \xleftarrow {\$}$ S-DH.

$\mathrm {P_6}$ and $\mathrm {P_5}$ are identical unless the doublepwserver event occurs, however, this only occurs with probability $\epsilon \le n^2_{ro} \cdot \mathrm {Adv}^\mathrm {CDH}_{G_q} (\hat{\mathcal {B}}^{\mathcal {A}})$. The quadratic degradation factor is due to $\hat{\mathcal {B}}^{\mathcal {A}}$ having to guess two queries $H_l(C,S,X^*,Y, \sigma _1, \pi _1)$ and $H_l(C,S,X^*,Y, \sigma _2, \pi _2)$ such that $\sigma _1 =$ DH ($X^* / M^{\pi _1}, Y$) and $\sigma _2 =$ DH ($X^* / M^{\pi _2}, Y$).    $\square$

Game $\mathbf {{G}_7}$ : Internal password oracle.

In protocol $\mathrm {P_7}$, we consider an internal password oracle $\mathcal {O}_{\pi }$ who handles every password request and is only available to the challenger. Specifically, the challenger queries the $\mathcal {O}_{\pi }$ to (i) assign passwords to users, (ii) answer Corrupt queries and (iii) determine if the correctpw event occurs.

Claim 9

For all adversaries $\mathcal {A}$, ${\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_6}(\mathcal {A})}\,\right] } = {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A})}\,\right] }$.

Proof

It follows from inspection.    $\square$

Claim 10

For all adversaries $\mathcal {A}$, ${\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A})}\,\right] } \le \frac{1}{2} + \frac{n_{se}}{2\cdot |D|}$.

Proof

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A})}\,\right] } = {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A}) \mid \text{ correctpw }}\,\right] } \cdot {\Pr \left[ \,{\text{ correctpw }}\,\right] } \nonumber \\ + \ {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A}) \mid \lnot \text{ correctpw }}\,\right] } \cdot {\Pr \left[ \,{\lnot \text{ correctpw }}\,\right] } \end{aligned}$$

(2)

We know from $\mathrm {P_6}$ that $\mathcal {A}$ can test at most one password per instance in an active attack, then ${\Pr \left[ \,{\text{ correctpw }}\,\right] } \le n_{se} / |D|$. We examine the second term of Eq. 2. The security experiment requires the adversary to make a Test query to some PFS-fresh instance $\varPi _{U}^{i}$ of his choice. It is easy to show that the view of $\mathcal {A}$ is independent of the sk on which she is challenged: (i) $\mathrm {P_1}$ prevents two or more instances accepting with the same sid, which would violate the partnering definition allowing $\mathcal {A}$ to trivially win, (ii) it follows from $\mathrm {P_4}$ that, before any Corrupt query, only instances that are paired instances can reach terminate state – and therefore be target of a Test query – and (iii) from $\mathrm {P_5}$ it holds that for such paired instances, the view of $\mathcal {A}$ is independent of sk for the session target of the Test query. Then ${\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A}) \mid \lnot \text{ correctpw }}\,\right] } = 1/2$.    $\blacksquare$

4 The SPAKE2 Protocol

4.1 Security of SPAKE2

SPAKE2 protocol is already proven secure in the FtG model [8] without considering any notion of forward secrecy. Here, we show that SPAKE2 also satisfies weak forward secrecy in the FtG model assuming the CDH problem is hard in $\mathbb {G}$. The security proof of SPAKE2 is similar to that of PFS-SPAKE2 protocol; the biggest difference is game ${\mathrm {G}_6}$, where $\mathcal {A}$ is prevented from testing two different passwords when she masquerades as C but also when masquerading as S. The later scenario does not occur in PFS-SPAKE2 since a client instance aborts the protocol whenever it receives an invalid key-confirmation code k.

Fig. 2.

SPAKE2 protocol.

Theorem 2

Let P be the protocol specified in Fig. 2 instantiated in group $\mathbb {G}$ and with passwords uniformly distributed over dictionary $D$. Let $\mathcal {A}$ be an adversary that runs in time t polynomial in $\lambda$, makes at most $n_{ex}$, $n_{se}$, $n_{ro}$ queries of type execute, send and random oracle. Then:

$$\begin{aligned} \small \mathrm {Adv}^{\mathrm {wFS}\text {-}\mathrm {FtG}}_P(\mathcal {A}) \le \frac{n_{se}}{|D|} + \mathcal {O} \left( \frac{(n_{se} + n_{ex})(n_{se} + n_{ex} + n_{ro})}{q} \text { } + \right. \\ \left. n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}({\mathcal {B}^{\mathcal {A}}}) + n_{se} n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\tilde{\mathcal {B}}^{\mathcal {A}}) +n^2_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\hat{\mathcal {B}}^{\mathcal {A}}) \right) , \end{aligned}$$

where $\mathcal {B}^{\mathcal {A}}$, $\tilde{\mathcal {B}}^{\mathcal {A}}$ and $\hat{\mathcal {B}}^{\mathcal {A}}$ are CDH-solver algorithms running in time $t' = \mathcal {O} ( t + (n_{se} + n_{ex} + n_{ro})\cdot t_{exp} )$, where $t_{exp}$ is the time for an exponentiation in $\mathbb {G}$.

Next we provide a sketch of the proof, where we simply write $\mathrm {Succ}^\mathrm {FtG}_{P_i}$ instead of $\mathrm {Succ}^{\mathrm {wFS}\text {-}\mathrm {FtG}}_{P_i}$ to denote the success probability of $\mathcal {A}$ winning in game $\mathrm {G_i}$:

Game $\mathbf {{G}_0}$ : Execution of original protocol.

Game $\mathbf {{G}_1}$ : Force uniqueness of honest instances.

If honest instances generate $X^*$ or $Y^*$ terms equals those seen in previous executions of the protocol, the the protocol stops and $\mathcal {A}$ fails.

$$\begin{aligned} \mathrm {Succ}^\mathrm {FtG}_{P_0} \le \mathrm {Succ}^\mathrm {FtG}_{P_1} + \mathcal {O} \left( \frac{(n_{se} + n_{ex})(n_{se} + n_{ex} + n_{ro})}{q} \right) . \end{aligned}$$

Game $\mathbf {{G}_2}$: Simulation without password.

The protocol is simulated without using password information, subsequent random oracle queries made by $\mathcal {A}$ are backpatch to generate consistent views. Also, $\mathcal {A}$ is forced to query the random oracle to compute $sk = H(\cdot )$.

$$\begin{aligned} \mathrm {Succ}^\mathrm {FtG}_{P_1} (\mathcal {A}) \le \mathrm {Succ}^\mathrm {FtG}_{P_2} (\mathcal {A}) + \mathcal {O}(n_{se} / 2^\kappa ). \end{aligned}$$

Game $\mathbf {{G}_3}$: No need to backpatch $\varvec{H_l(\cdot )}$ queries against Execute queries.

We can show that the view of an $\mathcal {A}$ running in time t against $\mathrm {P}_2$ is computationally indistinguishable from that of $P_3$ via a CDH reduction.

$$\begin{aligned} \mathrm {Succ}^\mathrm {FtG}_{P_2}(\mathcal {A}) = \mathrm {Succ}^\mathrm {FtG}_{P_3} (\mathcal {A}) + n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}( \mathcal {B}^{\mathcal {A}}). \end{aligned}$$

where $\mathcal {B}^{\mathcal {A}}$ is a CDH-solver algorithm running in time $t' = \mathcal {O} ( t + (n_{se} + n_{ex} + n_{ro})\cdot t_{exp} )$ and $t_{exp}$ the time for an exponentiation in $\mathbb {G}$.

Game $\mathbf {{G}_4}$ : Check for successful password guesses.

If before any Corrupt query, the adversary is successful on a password guess against a client or server instance, the protocol stops and the adversary wins.

$$\begin{aligned} \mathrm {Succ}^\mathrm {FtG}_{P_3} (\mathcal {A}) \le \mathrm {Succ}^\mathrm {FtG}_{P_4} (\mathcal {A}). \end{aligned}$$

Game $\mathbf {{G}_5}$: Randomized session keys for paired instances. We build a CDH-solver algorithm from an adversary who manages to compute the sk established at paired instances $\varPi _{C}^{i}$ and $\varPi _{S}^{j}$, even if $\mathcal {A}$ obtains $\pi _C$ by adaptively corrupting any of the instances.

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_4}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] } + n_{se} \cdot n_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\tilde{\mathcal {B}}^{\mathcal {A}}). \end{aligned}$$

Game $\mathbf {{G}_6}$: Prevent testing more than one passwords per instance.

If before any Corrupt query, $\mathcal {A}$ manages to test more than one passwords per client or server instance, the protocol stops and the adversary fails. Via a CDH reduction, we show this may happend only with negligible probability.

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_4}(\mathcal {A})}\,\right] } \le {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_5}(\mathcal {A})}\,\right] } + 2n^2_{ro} \cdot \mathrm {Adv}^{\mathtt {CDH}}_{\mathbb {G}}(\hat{\mathcal {B}}^{\mathcal {A}}). \end{aligned}$$

Game $\mathbf {{G}_7}$: Internal password oracle.

By inspection $\mathrm {P}_6$ is statistically indistinguishable from $\mathrm {P}_7$. Additionally, let $\varPi _{U}^{i}$ be any instance that remains wFS-fresh and is the target of a Test query. In $\mathrm {P}_7$, provided that $\mathcal {A}$ has not successfully guessed the password, the view of the adversary is independent of the $sk_U^i$. Then:

$$\begin{aligned} {\Pr \left[ \,{\mathrm {Succ}^\mathrm {FtG}_{P_7}(\mathcal {A})}\,\right] } = \frac{1}{2} + \frac{n_{se}}{2\cdot |D|} \end{aligned}$$

5 Conclusion and Future Work

We proved that SPAKE2 protocol satisfies weak forward secrecy. Note that proving perfect forward secrecy for unmodified SPAKE2 seems to be a harder task. Consider the following scenario: $\mathcal {A}$ masquerades as a client and sends an arbitrary message $X^*$ to a server instance $\varPi _{S}^{j}$, the latter computes $Y^*$, its session key, answers back with $Y^*$ and terminates. Now $\mathcal {A}$ makes a Test(S, j) query, receives the challenge and then corrupts the tested server instance (as corruption occurred after the Test query the instance $\varPi _{S}^{j}$ remains PFS-fresh). The difficulty is that, even though the proof shows that $\mathcal {A}$ cannot test two passwords per instance, in this particular scenario the simulator cannot determine the password to which $\mathcal {A}$ committed in $X^*$ as she has not asked any random oracle query. Given the difficulty in proving perfect forward secrecy for SPAKE2, we modified the protocol by incorporating key-confirmation codes into it. We proved that the modified protocol satisfies perfect forward secrecy and therefore we called it PFS-SPAKE2.

In future work, we would like to study if the SPAKE2 and PFS-SPAKE2 protocols compose securely with symmetric-key encryption schemes. This question has practical relevance, as in TLS 1.3 the aforementioned primitives would be used not in stand alone operation but as a combined system.

A Terminology from [3]

We introduce the terminology necessary to refer to adversary’s actions.

We say “in a CLIENT ACTION k query to $\varPi _{C}^{i}$” to refer to “in a Send query directed to the client instance $\varPi _{C}^{i}$ that results in CLIENT ACTION k procedure being executed” and “in a SERVER ACTION k” to refer to “in a Send query directed to the server instance $\varPi _{S}^{j}$ that results in SERVER ACTION k procedure being executed”.

A client instance $\varPi _{C}^{i}$ is paired with server instance $\varPi _{S}^{j}$ if there was a CLIENT ACTION 0 query to $\varPi _{C}^{i}$ with output $\langle C, X^* \rangle$, a SERVER ACTION 1 to $\varPi _{S}^{j}$ with input $\langle C, X^* \rangle$ and output $\langle S,Y,k \rangle$ and a CLIENT ACTION 1 to $\varPi _{C}^{i}$ with input $\langle S,Y,k \rangle$. A server instance $\varPi _{S}^{j}$ is paired with client instance $\varPi _{C}^{i}$ if there was a CLIENT ACTION 0 query to $\varPi _{C}^{i}$ with output $\langle C, X^* \rangle$ and a SERVER ACTION 1 to $\varPi _{S}^{j}$ with input $\langle C, X^* \rangle$ and output $\langle Y,k \rangle$, additionally, if there is a SERVER ACTION 2 query with input $k'$, then there was a previous CLIENT ACTION 1 to $\varPi _{C}^{i}$ with input $\langle Y,k \rangle$ and ouput $k'$.

Next we define the events that will allow us to proof the security of the protocol by sequence of games.

testpw($C,i,S,\pi ,l$): Adversary $\mathcal {A}$ makes (i) an $H_l(C,S,X^*,Y,\sigma ,\pi )$ query for some $l\in \{1,2,3\}$, (ii) a CLIENT ACTION 0 to $\varPi _{C}^{i}$ with output $\langle S,X^*\rangle$ and (iii) a CLIENT ACTION 1 to $\varPi _{C}^{i}$ with input $\langle C,Y,k \rangle$, where $X^* = X \cdot M^\pi$ and $\sigma =DH(X,Y)$. The associated value to this event is the output of the $H_l(\cdot )$ query, or the $k,k',sk_C^i$ values, respectively for $l=1,2,3$, whichever is set first.

testpw($S,j,C,\pi ,l$): $\mathcal {A}$ makes an $H_l(C,S,X^*,Y,\sigma ,\pi )$ for some $l\in \{1,2,3\}$ and a SERVER ACTION 1 to $\varPi _{S}^{j}$ with input $\langle S,X^*\rangle$ and output $\langle C,Y,k \rangle$, where $X^* = X \cdot M^{\pi }$ and $\sigma = DH(X,Y)$. The associated value to this event is the output of the $H_l(\cdot )$ query, or the $k,k',sk_S^j$ values, respectively for $l=1,2,3$, whichever is set first.

testpw!($C,i,S,\pi$): In a CLIENT ACTION 1 query with input $\langle \mu ,k \rangle$, causes a testpw$(C,i,S,\pi ,2)$ event to occurs, with associated value k.

testexecpw($C,i,S,j,\pi$): $\mathcal {A}$ makes (i) an $H_l(C,S,X^*,Y,\sigma ,\pi )$ for some $l\in \{1,2,3\}$, where $X^* = X \cdot M^\pi$ and $\sigma =DH(X,Y)$ and (ii) previously an Execute(C, i, S, j) which produces $X^*,Y$. The associated value to this event is the output of the $H_l(\cdot )$ query, or the $k,k',sk_S^j$ values, respectively for $l=1,2,3$, whichever is set first.

correctpw: Before any Corrupt query, either a testpw!($C,i,S,\pi _c$) event occurs, for some C, i, S, or a testpw($S,j,C,\pi _c,l$) event occurs for some S, j, C and $l\in \{1,2,3\}$, where $\pi _c$ is the correct password.

pairedpwguess: For some client and server instance $\varPi _{C}^{i}$ and $\varPi _{S}^{j}$ respectively, both testpw($C,i,S,\pi _c,l$) and testpw($S,j,C,\pi ,l$) event occurs for $l\in \{1,2,3\}$, where $\varPi _{C}^{i}$ is paired with $\varPi _{S}^{j}$, and $\varPi _{S}^{j}$ is paired with $\varPi _{C}^{i}$ after its SERVER ACTION 1.

doublepwserver: Before any Corrupt query, both a testpw($S,j,C,\pi _1,l$) and a testpw($S,j,C,\pi _2,l$) event occurs, for some S, j, $\pi _1$ and $\pi _2$, with $\pi _1 \ne \pi _2$ and $l \in \{1,2,3\}$.