F-KE — Key exchange, strong with forward secrecy

F-KE (Key exchange, strong with forward secrecy) is part of Public-Key Primitives, Key Exchange, Messaging in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

Two parties name each other, and one uniformly random key comes out — the same key for both, and one the adversary never sees unless it had already corrupted an endpoint. The box is small, and the reason it is interesting is that its own authors show it is too strong: the two-move Diffie–Hellman protocol does not realize it, and the paper’s main technical contribution is a deliberately weakened sibling that SK-secure protocols do realize.

Functionality

Reading the box: $\mathcal{A}(\cdot)$ is a call on the adversary slot whose answer is not used, so it is a notification rather than a query; $\mathsf{San}[\mathsf{Clean}_{k}]$ replaces an answer failing the predicate with $\bot$; $\square$ marks a value never set; require refuses the call, and the framework answers $\textsf{rej}$, so no return is written for it; $\kappa$, the parameter on the header line, is the key length.

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

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

Initialize():

$\mathtt{Peer} : \mathcal{F}_{\mathsf{KE}}.\mathbf{P} \to \mathcal{F}_{\mathsf{KE}}.\mathbf{P} \cup \{\square\}$
$\mathtt{Peer}[*] \gets \square$// who asked to talk to whom
$\mathtt{Role} : \mathcal{F}_{\mathsf{KE}}.\mathbf{P} \to \{\mathsf{ini}, \mathsf{res}\} \cup \{\square\}$
$\mathtt{Role}[*] \gets \square$
$\mathtt{A} \gets \square$; $\mathtt{B} \gets \square$// the matched pair, in the order they asked
$\mathtt{k} \gets \square$
$\mathtt{out}[*] \gets 0$

id.Establish(Q, r)from id′

$\textbf{require}\ \mathtt{Peer}[\mathit{id}.P] = \square \ \wedge\ Q \neq \mathit{id}.P \ \wedge\ \mathtt{k} = \square$// one request per party, and only before a key exists
$\mathtt{Peer}[\mathit{id}.P] \gets Q$; $\mathtt{Role}[\mathit{id}.P] \gets r$
$\mathcal{A}\bigl(\mathit{id}.\mathsf{Establish},\ \mathit{id}.P,\ Q,\ r\bigr)$// the whole tuple, role included
$\textbf{if}\ \mathtt{Peer}[Q] \neq \mathit{id}.P\ \textbf{then}$
$\textbf{return}$ ok// no matching request yet
$\mathtt{A} \gets Q$; $\mathtt{B} \gets \mathit{id}.P$
$\textbf{if}\ \{\mathtt{A}, \mathtt{B}\} \cap \mathbf{C} = \varnothing\ \textbf{then}$
$\mathtt{k} \gets_{\$} \{0,1\}^{\kappa}$
$\mathcal{A}\bigl(\mathit{id}.\mathsf{Establish},\ \mathsf{Key},\ \mathtt{A},\ \mathtt{B}\bigr)$// that a key exists, never which
$\textbf{if}\ \{\mathtt{A}, \mathtt{B}\} \cap \mathbf{C} \neq \varnothing\ \textbf{then}$
$\mathtt{k} \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Establish},\ \mathsf{Choose},\ \mathtt{A},\ \mathtt{B}\bigr)$
$\mathtt{k} \gets \mathsf{San}[\mathsf{Clean}_{k}](\mathtt{k})$
$\textbf{return}$ ok

id.Fetch()from id′

$\textbf{require}\ \mathit{id}.P \in \{\mathtt{A}, \mathtt{B}\} \ \wedge\ \mathtt{k} \neq \square \ \wedge\ \mathtt{out}[\mathit{id}.P] = 0$
$\mathtt{out}[\mathit{id}.P] \gets 1$
$\textbf{return}\ \mathtt{k}$

id.Leak()from id′

$\textbf{if}\ \mathit{id}.P \notin \{\mathtt{A}, \mathtt{B}\}\ \textbf{then}$
$\textbf{return}\ (\mathtt{A},\ \mathtt{B})$// an outsider learns who, never the key
$\textbf{if}\ \mathtt{out}[\mathit{id}.P] = 0\ \textbf{then}$
$\textbf{return}\ (\mathtt{Peer}[\mathit{id}.P],\ \mathtt{Role}[\mathit{id}.P],\ \mathtt{k})$// before delivery, and only then
$\textbf{return}\ (\mathtt{Peer}[\mathit{id}.P],\ \mathtt{Role}[\mathit{id}.P])$

Clean_k(k):

$\textbf{return}\ k \in \{0,1\}^{\kappa}$

The box is transcribed from Canetti and Krawczyk, Universally composable notions of key exchange and secure channels, ePrint 2002/059, revision 20020514:200902, Figure 7, PDF p. 31 (printed p. 29) — the functionality $\mathcal{F}_{\textsc{ke}}$, “The (Strong) Key Exchange functionality”. The posting has exactly one revision and exists only as PostScript; the PDF read here was produced from 2002/059.ps with Ghostscript, so its page numbering is the PostScript’s own.

Three readings the box commits to, each visible in one line:

Line 10 reports the role and line 11 ignores it. The source is explicit on both halves: the tuple sent to the adversary carries $\mathit{role}$, and the matching test fires on a recorded $(\mathit{sid}, P_j, P_i, \mathit{role}')$ “either with $\mathit{role}' \neq \mathit{role}$ or $\mathit{role}' = \mathit{role}$”. The paper says why — the field “plays no security role in the definition”, and is there only so that a KE protocol’s input format matches the one its SK-security definition uses. This is the sharpest single difference from F-SC in the same paper, which does require the roles to be complementary before a session becomes active.
Line 15 against line 18 is the whole corruption model. With both endpoints honest the key is drawn uniformly and the adversary is told only that a key exists and between whom. With either endpoint corrupt the adversary supplies the key outright. There is no middle case, and no leakage function: the box either hands the adversary full control of the key or none of it.
Line 27 is the forward-secrecy clause, and line 22 is the boundary it turns on. The source’s step 2 provides the adversary with the session key on corruption “if the session key is not yet sent (i.e., it was not yet written on the outgoing communication tape)”. Here delivery is a pull, so “sent” is the flag $\mathtt{out}$ set by that party’s own $\mathsf{Fetch}$.

Where the source is silent and this box has to decide:

Source	Box	Why
Sends $(\texttt{key}, \mathit{sid}, \kappa)$ to both parties	$\mathsf{Fetch}$ returns $\mathtt{k}$ to the caller	Delivery is a pull here. The source gives the adversary no say over when the key arrives, so $\mathsf{Fetch}$ places no call on the adversary slot — which is exactly what distinguishes this box from the relaxed variant below.
“and halt” after the exchange	Line 8’s $\mathtt{k} = \square$ test, and $\mathtt{out}$	One key per instance, and one delivery per partner. The instance stays alive rather than dying, so a second $\mathsf{Establish}$ is refused rather than lost.
“if the session key is not yet sent” — singular, though the source writes two messages	Per-party: $\mathtt{out}[\mathit{id}.P]$	The source’s two writes are separate activations, so the flag could be global or per-party and the text does not say. Read per-party, a partner who has not yet fetched still leaks the key even after its peer has taken it. Read globally, the first fetch would close the window for both. The per-party reading is the weaker of the two and therefore the safe one to transcribe.
No $\mathsf{Leak}$	Lines 24–28	Required on every box here. What an outsider gets is the pair of identities; what a partner gets is its own request, plus the key iff it has not yet fetched. Nothing else in the box’s state is secret.
No condition on the named peer	Line 8 adds $Q \neq \mathit{id}.P$	An addition, and declared as one: the source lets $P_i$ name itself, and the matching test at line 11 would then fire on that single request and produce a one-party “exchange”. Nothing in the source suggests that is intended, and no protocol realizes it.
Static corruption, tested once	$\mathtt{C}$ tested at line 14 and line 17	Corruption after line 15 is handled by $\mathsf{Leak}$, not by re-running the branch — the key is drawn and stays drawn.

Known realizations

In the paper the box is taken from:

Theorem 9: if the Decisional Diffie–Hellman assumption holds, protocol SIG-DH securely realizes $\mathcal{F}_{\textsc{ke}}$ in the $\mathcal{F}_{\textsc{sig}}$-hybrid model. SIG-DH is ISO 9798-3 Diffie–Hellman authenticated with signatures. The paper does not prove this directly; it follows from its Theorem 14 together with SIG-DH being SK-secure under DDH and satisfying the paper’s ACK property.
Claim 11: protocol 2DH — two-move Diffie–Hellman — does not securely realize $\mathcal{F}_{\textsc{ke}}$ in the authenticated-links model, even without forward secrecy, despite being SK-secure.

Claim 11 is why this entry has a sibling in the same paper. $\mathcal{F}^{\mathcal{N}}_{\textsc{rke}}$ (Figure 10, PDF p. 38, printed p. 36) is $\mathcal{F}_{\textsc{ke}}$ with two changes: the key is produced by a non-information oracle $\mathcal{N}$ whose internal state the adversary gets on early corruption instead of the key itself, and delivery to each party waits for an explicit $(\texttt{ok}, \mathit{sid}, l)$ from the adversary. Both changes weaken the box, and both are needed: under DDH there is a non-information oracle for which 2DH does realize $\mathcal{F}^{\mathcal{N}}_{\textsc{rke}}$ in the authenticated-links model (Claim 18), and more generally every SK-secure protocol realizes it for some non-information oracle (Claim 20), which is the paper’s equivalence between relaxed UC security and SK-security.

This encyclopedia has no page for the relaxed variant. That is a gap rather than a decision: $\mathcal{F}^{\mathcal{N}}_{\textsc{rke}}$ is the functionality the key-exchange literature actually realizes, and it is a different object, not a restatement.

Properties

Key secrecy against an outsider, with probability exactly $0$ of leakage: with both endpoints honest, no return value and no call on the adversary slot is a function of $\mathtt{k}$ except line 27, which requires the caller to be a partner. Line 25 hands over the identities and nothing more.
Agreement, with probability exactly $1$: there is one $\mathtt{k}$ per instance and $\mathsf{Fetch}$ returns it unmodified, so two partners that both fetch hold the same string. The adversary cannot substitute one endpoint’s key for another’s, which is the property 2DH retains and the one an unauthenticated protocol loses.
Forward secrecy, conditional rather than unconditional: the key survives corruption only after the corrupted party has fetched it. Corrupting either endpoint before its $\mathsf{Establish}$ puts the adversary in the line-18 branch, where it names the key; corrupting between line 15 and that party’s $\mathsf{Fetch}$ reaches line 27. The paper states the same boundary and notes that dropping the clause — letting the adversary learn the key on corruption at any time — is what it means by strong UC security without PFS.
One key, one session. The parameter set carries no session count, and line 8 refuses a second exchange. The multi-session case is the source’s multi-session extension, not this box.

Formal artifacts

No machine-checked formalization yet.

References:

Canetti and Krawczyk. Universally composable notions of key exchange and secure channels. In Advances in Cryptology – EUROCRYPT 2002, volume 2332 of LNCS, pages 337–351, 2002. Figure 7, PDF p. 31 (printed p. 29) of revision 20020514:200902, the definition transcribed above; Figure 10, PDF p. 38 (printed p. 36) for the relaxed variant; Theorem 9 and Claims 11, 18 and 20.
Canetti and Krawczyk. Analysis of key-exchange protocols and their use for building secure channels. In Advances in Cryptology – EUROCRYPT 2001, volume 2045 of LNCS, pages 453–474, 2001. Where SK-security and the SIG-DH and 2DH protocols come from; it predates the functionality and prints no box for it.
Bellare and Rogaway. Entity authentication and key distribution. In Advances in Cryptology – CRYPTO 1993, volume 773 of LNCS, pages 232–249, 1994. The indistinguishability-based ancestor of SK-security, likewise with no functionality to transcribe.

Source	Box	Why
Sends \((\texttt{key}, \mathit{sid}, \kappa)\) to both parties	\(\mathsf{Fetch}\) returns \(\mathtt{k}\) to the caller	Delivery is a pull here. The source gives the adversary no say over when the key arrives, so \(\mathsf{Fetch}\) places no call on the adversary slot — which is exactly what distinguishes this box from the relaxed variant below.
“and halt” after the exchange	Line 8’s \(\mathtt{k} = \square\) test, and \(\mathtt{out}\)	One key per instance, and one delivery per partner. The instance stays alive rather than dying, so a second \(\mathsf{Establish}\) is refused rather than lost.
“if the session key is not yet sent” — singular, though the source writes two messages	Per-party: \(\mathtt{out}[\mathit{id}.P]\)	The source’s two writes are separate activations, so the flag could be global or per-party and the text does not say. Read per-party, a partner who has not yet fetched still leaks the key even after its peer has taken it. Read globally, the first fetch would close the window for both. The per-party reading is the weaker of the two and therefore the safe one to transcribe.
No \(\mathsf{Leak}\)	Lines 24–28	Required on every box here. What an outsider gets is the pair of identities; what a partner gets is its own request, plus the key iff it has not yet fetched. Nothing else in the box’s state is secret.
No condition on the named peer	Line 8 adds \(Q \neq \mathit{id}.P\)	An addition, and declared as one: the source lets \(P_i\) name itself, and the matching test at line 11 would then fire on that single request and produce a one-party “exchange”. Nothing in the source suggests that is intended, and no protocol realizes it.
Static corruption, tested once	\(\mathtt{C}\) tested at line 14 and line 17	Corruption after line 15 is handled by \(\mathsf{Leak}\), not by re-running the branch — the key is drawn and stays drawn.