F-saPAKE — Strong asymmetric PAKE

F-saPAKE (Strong asymmetric PAKE) is part of Public-Key Primitives, Key Exchange, Messaging in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

The strong asymmetric PAKE is the weak one with the pre-computation attack taken away. Compare line 11 here with lines 10–11 of F-aPAKE: stealing the password file returns the token $\textsf{stolen}$ and nothing else, and line 12 refuses every offline guess until the theft has happened. An adversary that spends a year building a rainbow table before the breach gains nothing by it — the dictionary search can only start at the moment of compromise. That is the property OPAQUE was built to have, and the definition is where it is stated.

Two mechanisms are added to pay for it, and both are visible in the box. $\mathtt{Flag}$ (lines 7, 14, 35) tracks whether the password itself has been broken, as opposed to the file merely being stolen; and $\mathtt{Dpt}$ with $\mathsf{Interrupt}$ (lines 25–27, 32–33) gives the adversary one deferred password test against the server, which is what a real protocol leaks when it interferes with a server session and tests later.

Functionality

Reading the box: $\mathcal{A}(\cdot)$ is a call on the adversary slot and $\mathit{id}'.F = \mathbf{A}$ tests that the adversary is the caller; require refuses the call, and the framework answers $\textsf{rej}$; $\mathbf{C}$ is the set of corrupted parties; $\square$ marks a value never set; $t$ is a sub-session identifier, so $\mathtt{St}[t,P]$ is the state of party $P$’s session $t$ and $\bar{P}$ is the peer; $U$, $S$ and $\lambda$ are parameters.

Functionality $\mathcal{F}_{\mathsf{saPAKE}}$

$\mathit{pid}$, $\mathbf{P}$, $\mathbf{N}$, $\mathbf{U} := \{(\mathcal{A},\mathsf{serves})\}$, $\mathit{par} := (U, S, \lambda)$

Initialize():

$\mathtt{Pw} \gets \square$; $\mathtt{Stolen}, \mathtt{Flag} \gets 0$
$\mathtt{St} : \mathcal{I} \times \mathbf{P} \to \{\mathsf{fresh}, \mathsf{intr}, \mathsf{comp}, \mathsf{done}\} \cup \{\square\}$
$\mathtt{Guess}, \mathtt{Key} : \mathcal{I} \times \mathbf{P} \to \{0,1\}^* \cup \{\square\}$
$\mathtt{Dpt} : \mathcal{I} \to \{0,1\}$; $\mathtt{Dpt}[*] \gets 0$
$\mathtt{St}[*,*], \mathtt{Guess}[*,*], \mathtt{Key}[*,*] \gets \square$

id.StorePwdFile(pw)from id′

$\textbf{require}\ \mathit{id}.P = S \ \wedge\ \mathtt{Pw} = \square$
$\mathtt{Pw} \gets \mathit{pw}$; $\mathtt{Flag} \gets 0$// $\mathtt{Flag}$: has the password itself been broken
$\textbf{return}$ ok

id.StealPwdFile()from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{Pw} \neq \square$
$\mathtt{Stolen} \gets 1$
$\textbf{return}\ \mathsf{stolen}$// the file, and nothing else: no pre-computation

id.OfflineTestPwd(mathit{pw}^{*})from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{Stolen} = 1$// guessing starts only after the theft
$\textbf{if}\ \mathit{pw}^{*} = \mathtt{Pw}\ \textbf{then}$
$\mathtt{Flag} \gets 1$
$\textbf{return}$ true
$\textbf{return}$ false

id.UsrSession(t, mathit{pw}')from id′

$\textbf{require}\ \mathit{id}.P = U \ \wedge\ \mathtt{St}[t,U] = \square$
$\mathtt{St}[t,U] \gets \mathsf{fresh}$; $\mathtt{Guess}[t,U] \gets \mathit{pw}'$
$\mathcal{A}\bigl(\mathit{id}.\mathsf{UsrSession}, t\bigr)$
$\textbf{return}$ ok

id.SvrSession(t)from id′

$\textbf{require}\ \mathit{id}.P = S \ \wedge\ \mathtt{Pw} \neq \square \ \wedge\ \mathtt{St}[t,S] = \square$
$\mathtt{St}[t,S] \gets \mathsf{fresh}$; $\mathtt{Guess}[t,S] \gets \mathtt{Pw}$
$\mathcal{A}\bigl(\mathit{id}.\mathsf{SvrSession}, t\bigr)$
$\textbf{return}$ ok

id.Interrupt(t)from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{St}[t,S] = \mathsf{fresh}$
$\mathtt{St}[t,S] \gets \mathsf{intr}$; $\mathtt{Dpt}[t] \gets 1$// buys one deferred guess against the server
$\textbf{return}$ ok

id.TestPwd(t, P, mathit{pw}^{*})from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{St}[t,P] \neq \square$
$b \gets \bigl(\mathit{pw}^{*} = \mathtt{Guess}[t,P]\bigr)$
$\textbf{if}\ \mathtt{St}[t,P] = \mathsf{fresh}\ \textbf{then}$
$\mathtt{St}[t,P] \gets \mathsf{comp}\ \textbf{if}\ b\ \textbf{else}\ \mathsf{intr}$
$\textbf{if}\ \mathtt{St}[t,P] \neq \mathsf{fresh} \ \wedge\ P = S \ \wedge\ \mathtt{Dpt}[t] = 1\ \textbf{then}$
$\mathtt{Dpt}[t] \gets 0$// the deferred guess, spent
$\textbf{if}\ P = S \ \wedge\ b\ \textbf{then}$
$\mathtt{Flag} \gets 1$// a correct guess at the server breaks the password
$\textbf{return}\ b$

id.Impersonate(t)from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{St}[t,U] = \mathsf{fresh}$
$\textbf{if}\ \mathtt{Flag} = 1 \ \wedge\ \mathtt{Guess}[t,U] = \mathtt{Pw}\ \textbf{then}$
$\mathtt{St}[t,U] \gets \mathsf{comp}$// the file alone is not enough; the password is
$\textbf{return}$ true
$\mathtt{St}[t,U] \gets \mathsf{intr}$
$\textbf{return}$ false

id.NewKey(t, P, k^{*})from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{St}[t,P] \notin \{\square, \mathsf{done}\} \ \wedge\ |k^{*}| = \lambda$
$\textbf{if}\ \mathtt{St}[t,P] = \mathsf{comp} \ \vee\ P \in \mathbf{C} \ \vee\ \bar{P} \in \mathbf{C}\ \textbf{then}$
$\mathtt{Key}[t,P] \gets k^{*}$
$\textbf{if}\ P = S \ \wedge\ \mathtt{St}[t,P] = \mathsf{intr} \ \wedge\ \mathtt{Flag} = 1\ \textbf{then}$
$\mathtt{Key}[t,P] \gets k^{*}$// a broken password lets the server be driven
$\textbf{if}\ \mathtt{St}[t,P] = \mathsf{fresh} \ \wedge\ \mathtt{St}[t,\bar{P}] = \mathsf{done} \ \wedge\ \mathtt{Guess}[t,P] = \mathtt{Guess}[t,\bar{P}]\ \textbf{then}$
$\mathtt{Key}[t,P] \gets \mathtt{Key}[t,\bar{P}]$
$\textbf{if}\ \mathtt{Key}[t,P] = \square\ \textbf{then}$
$\mathtt{Key}[t,P] \gets \$\,\{0,1\}^{\lambda}$
$\mathtt{St}[t,P] \gets \mathsf{done}$
$\textbf{return}\ \mathtt{Key}[t,P]$ to $P$

id.TestAbort(t, P)from id′

$\textbf{require}\ \mathit{id}'.F = \mathbf{A} \ \wedge\ \mathtt{St}[t,P] \notin \{\square, \mathsf{done}\}$
$\textbf{if}\ \mathtt{St}[t,P] = \mathsf{fresh} \ \wedge\ \mathtt{St}[t,\bar{P}] \neq \square\ \textbf{then}$
$\textbf{return}\ \mathsf{succ}$
$\textbf{if}\ \mathtt{St}[t,P] = \mathsf{fresh} \ \wedge\ \bar{P} = S \ \wedge\ \mathtt{Guess}[t,P] = \mathtt{Pw}\ \textbf{then}$
$\textbf{return}\ \mathsf{succ}$// a correct password cannot be made to abort
$\mathtt{St}[t,P] \gets \mathsf{done}$
$\textbf{return}\ \mathsf{fail}$, and $\mathsf{abort}$ to $P$

id.Leak()from id′

$\textbf{if}\ \mathit{id}.P = S\ \textbf{then}$
$\textbf{return}\ (\mathtt{Pw}, \mathtt{Stolen}, \mathtt{Flag}, \mathtt{St})$
$\textbf{return}\ (\mathtt{Stolen}, \mathtt{St})$

Source: Figure 2, p. 9 of Jarecki, Krawczyk and Xu, “OPAQUE: An Asymmetric PAKE Protocol Secure Against Pre-computation Attacks”, ePrint 2018/163, revision 20191022:184539, the newest of nine postings. The PDF’s pages and its printed folios agree.

Figure 2 is a diff, and the box above is the assembled result. Its caption reads “Functionality $\mathcal{F}_{\mathsf{saPAKE}}$ with marked additions relative to $\mathcal{F}_{\mathsf{saPAKE+}}$”, and $\mathcal{F}_{\mathsf{saPAKE+}}$ is itself Figure 1 with its shaded lines deleted. So reading this functionality correctly needs both figures and both shadings: Figure 1 minus its shading, plus Figure 2’s marked additions. That is three documents’ worth of state encoded in two figures’ typography, and it does not survive a text extraction — the additions here are lines 7, 14, 25–27, 32–35, 46–47 and 57–58.

Line 11 is the entire strength claim. No pre-computation record exists in this box at all — there is no counterpart to the weak version’s $\mathtt{Off}$ set — so a theft yields the file and nothing more.
Line 12 is its enforcement. Offline guessing requires $\mathtt{Stolen} = 1$. Before the breach the adversary may not even ask, which is the formal content of “secure against pre-computation attacks”.
Lines 34–35 set $\mathtt{Flag}$, and it is the distinction the weak box lacks. $\mathtt{Stolen}$ says the file is out; $\mathtt{Flag}$ says the password is known. In the weak version these collapse, because the file plus a precomputed table is the password. Here they come apart, and every downstream privilege is gated on $\mathtt{Flag}$ rather than $\mathtt{Stolen}$ — see line 38.
Line 38 is the impersonation rule, and it is strictly weaker than the weak box’s. There, $\mathtt{Stolen} = 1$ sufficed to impersonate the server. Here the adversary needs $\mathtt{Flag} = 1$: it must actually have found the password, by exhaustive search after the theft. Stealing the file no longer impersonates anybody for free.
Lines 25–27 and 32–33 are the deferred test, and the accounting is the subtle part. $\mathsf{Interrupt}$ moves a fresh server session to $\mathsf{intr}$ and sets $\mathtt{Dpt}[t] = 1$; a later $\mathsf{TestPwd}$ against that session spends the credit at line 33. Without this the functionality would be stronger than any protocol can be — a real adversary that garbles a server flow learns, later, whether its guess was right. The credit is one per interrupt, and line 33 clears it.
Lines 46–47 are the concession that a broken password buys. An interrupted server session, once $\mathtt{Flag}$ is set, takes the adversary’s key. This is narrower than it looks: it needs the password and an interrupt, and it applies to the server’s side only.
Lines 57–58 are the other addition to $\mathsf{TestAbort}$: a fresh session whose peer is the server and whose password is correct cannot be made to abort. A correct password is entitled to succeed.

Mismatch register.

The source	This box	Why
Figure 2 as a marked diff over $\mathcal{F}_{\mathsf{saPAKE+}}$, itself a shading-diff over Figure 1	The assembled functionality	A diff is not a definition. The additions are named above so the diff is recoverable.
`if the record is FRESH ... else if P = S and dPT(ssid) = 1`	Lines 30–31 and 32–33, two guarded `if`s	The generator’s LaTeX subset has no `else if`; the second guard carries the negation ($\mathtt{St}[t,P] \neq \mathsf{fresh}$), so the priority is preserved.
Records keyed by $\langle \mathit{ssid}, P, P', \mathit{pw}'\rangle$	$\mathtt{St}$, $\mathtt{Guess}$, $\mathtt{Key}$ keyed by $(t, P)$	As in the weak box: $\mathit{sid}$ folds into the process id, $\mathit{ssid}$ cannot, and the per-party split must be kept.
$\mathsf{flag}$ on the file record	$\mathtt{Flag}$, an instance-level boolean	One file per instance, so no key is needed.
No leakage interface	$\mathsf{Leak}$ at lines 61–63	Required here. A corrupted server loses the password, the theft state and $\mathtt{Flag}$; anyone else learns only the public schedule.

Known realizations

OPAQUE: Figure 4, in the $(\mathcal{F}_{\mathsf{OPRF}}, \mathcal{F}_{\mathsf{aPAKE}})$-hybrid world. The construction composes an oblivious PRF with the weak asymmetric PAKE of F-aPAKE and realizes this functionality. The OPRF is what removes the pre-computation: the password is never hashed alone, only through a server-keyed PRF the adversary cannot evaluate offline before it holds the key. So the two boxes on this site stand in a realization relation, not merely a comparison.

A second route: Figure 8. OPRF-AKE builds a strong aPAKE from an AKE with key-compromise impersonation resistance and an OPRF, with the corresponding functionality $\mathcal{F}_{\mathsf{AKE-KCI}}$ printed in Figure 7.

Properties

No pre-computation advantage, with probability exactly $1$. Line 12 refuses every offline guess before the theft, and no state records pre-theft attempts. The adversary’s offline work provably cannot start early. This is the property the whole paper is named for and it is one require.
One offline guess per call after theft. Lines 12–16. Inherent, and unchanged from the weak notion.
One online guess per session, plus one deferred guess per interrupt. Lines 28–33. The deferred credit is the only addition to the online budget, and line 33 spends it.
Server impersonation requires the password, not the file, with probability exactly $1$. Line 38, gated on $\mathtt{Flag}$.
Key secrecy for unbroken sessions, with advantage exactly $0$. Line 51, reachable only when lines 44, 46 and 48 all failed to fire.
Key agreement for matching honest sessions, with probability exactly $1$. Lines 48–49.

Formal artifacts

No machine-checked formalization yet.

References:

Jarecki, Krawczyk, and Xu. OPAQUE: An asymmetric PAKE protocol secure against pre-computation attacks. In Advances in Cryptology – EUROCRYPT 2018, volume 10822 of LNCS, pages 456–486, 2018. The definition transcribed above is Figure 2, p. 9 of ePrint 2018/163, revision 20191022:184539, the newest of nine postings, read together with Figure 1 (p. 8) whose unshaded text is the $\mathcal{F}_{\mathsf{saPAKE+}}$ that Figure 2 modifies. The realizations are Figure 4 (in the $(\mathcal{F}_{\mathsf{OPRF}}, \mathcal{F}_{\mathsf{aPAKE}})$-hybrid world) and Figure 8; the auxiliary functionalities are $\mathcal{F}_{\mathsf{OPRF}}$ with adaptive compromise (Figure 3) and $\mathcal{F}_{\mathsf{AKE-KCI}}$ (Figure 7).