F-SE — Symmetric encryption, stream cipher

F-SE (Symmetric encryption, stream cipher) is part of Cryptographic Library and Symmetric Primitives in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

Functionality

Reading the box: \(\square\) marks a key never generated; \(\bot\) is a call the functionality has nothing to answer for. \(\mathtt{Known}\) tracks which keys the simulator already has real access to. \(\mathtt{DecTable}\) is the functionality’s own memory, per unknown key, of every (plaintext, ciphertext) pair it has produced — the only pairs an honest decryption is ever allowed to recover. \(L\) is the box’s own parameter: a leakage algorithm fixing exactly what an encryption under an unknown key discloses about the plaintext (its length, typically) while hiding the rest.

Functionality \(\mathcal{F}_{\mathsf{SE}}\)
\(\mathit{pid}\),   \(\mathbf{P}\),   \(\mathbf{N}\),   \(\mathbf{U} := \{(\mathcal{A},\mathsf{serves})\}\),   \(\mathit{par} := L\)
Initialize():
  1. \(\mathtt{Keys}, \mathtt{Known} \gets \varnothing\)
  2. \(\mathtt{Key} : \mathcal{F}_{\mathsf{SE}}.\mathbf{P} \times \mathbb{N} \rightharpoonup \mathtt{Keys}\)
  3. \(\mathtt{Next} : \mathcal{F}_{\mathsf{SE}}.\mathbf{P} \to \mathbb{N}\)
  4. \(\mathtt{Next}[*] \gets 0\)
  5. \(\mathtt{DecTable} : \mathtt{Keys} \to 2^{\{0,1\}^{*} \times \{0,1\}^{*}}\)
  6. \(\mathtt{DecTable}[*] \gets \varnothing\)
id.KeyGen()from id′
  1. \((\mathit{corr}, k) \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{KeyGen}\bigr)\)
  2. \(k \gets \mathsf{San}[\mathsf{Clean}_{k}](k; \mathtt{Keys})\)
  3. \(\mathtt{Keys} \gets \mathtt{Keys} \cup \{k\}\)
  4. \(\textbf{if}\ \mathit{corr} = 1\ \textbf{then}\)
  5. \(\mathtt{Known} \gets \mathtt{Known} \cup \{k\}\)
  6. \(\mathit{ptr} \gets \mathtt{Next}[\mathit{id}.P]\);  \(\mathtt{Next}[\mathit{id}.P] \gets \mathit{ptr} + 1\)
  7. \(\mathtt{Key}[\mathit{id}.P, \mathit{ptr}] \gets k\)
  8. \(\textbf{return}\ \mathit{ptr}\)
id.Store(k)from id′
  1. \(\textbf{if}\ k \in \mathtt{Keys} \setminus \mathtt{Known}\ \textbf{then}\)
  2. \(\textbf{return}\ \bot\)// a bare guess of an unknown key is refused
  3. \(\mathtt{Keys} \gets \mathtt{Keys} \cup \{k\}\);  \(\mathtt{Known} \gets \mathtt{Known} \cup \{k\}\)
  4. \(\mathit{ptr} \gets \mathtt{Next}[\mathit{id}.P]\);  \(\mathtt{Next}[\mathit{id}.P] \gets \mathit{ptr} + 1\)
  5. \(\mathtt{Key}[\mathit{id}.P, \mathit{ptr}] \gets k\)
  6. \(\textbf{return}\ \mathit{ptr}\)
id.Enc(ptr, msg)from id′
  1. \(k \gets \mathtt{Key}[\mathit{id}.P, \mathit{ptr}]\)
  2. \(\textbf{if}\ k = \square\ \textbf{then}\)
  3. \(\textbf{return}\ \bot\)
  4. \(c \gets \bot\)
  5. \(\textbf{if}\ k \notin \mathtt{Known}\ \textbf{then}\)
  6. \(c \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Enc}, L(\mathit{msg})\bigr)\)
  7. \(c \gets \mathsf{San}[\mathsf{Clean}_{c}](c)\)
  8. \(\textbf{if}\ c \neq \bot\ \textbf{then}\)
  9. \(\mathtt{DecTable}[k] \gets \mathtt{DecTable}[k] \cup \{(\mathit{msg}, c)\}\)
  10. \(\textbf{if}\ k \in \mathtt{Known}\ \textbf{then}\)
  11. \(c \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Enc}, \mathit{msg}\bigr)\)
  12. \(\textbf{return}\ c\)
id.Dec(ptr, c)from id′
  1. \(k \gets \mathtt{Key}[\mathit{id}.P, \mathit{ptr}]\)
  2. \(\textbf{if}\ k = \square\ \textbf{then}\)
  3. \(\textbf{return}\ \bot\)
  4. \(\mathit{msg} \gets \bot\)
  5. \(\textbf{if}\ k \notin \mathtt{Known}\ \textbf{then}\)
  6. \(\textbf{if}\ \exists!\, \mathit{msg}' : (\mathit{msg}', c) \in \mathtt{DecTable}[k]\ \textbf{then}\)
  7. \(\mathit{msg} \gets \mathit{msg}'\)// unique match; otherwise stays refused
  8. \(\textbf{if}\ k \in \mathtt{Known}\ \textbf{then}\)
  9. \(\mathit{msg} \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Dec}, c\bigr)\)
  10. \(\textbf{return}\ \mathit{msg}\)
id.Leak()from id′
  1. \(\textbf{return}\ \bigl(\{(\mathit{ptr}, \mathtt{Key}[\mathit{id}.P, \mathit{ptr}])\}_{\mathit{ptr} < \mathtt{Next}[\mathit{id}.P]}, \{(k, \mathtt{DecTable}[k]) : \exists\, \mathit{ptr}\, .\ \mathtt{Key}[\mathit{id}.P,\mathit{ptr}] = k\}\bigr)\)
Cleank(k; Keys):
  1. \(\textbf{return}\ k \in \{0,1\}^{*} \ \wedge\ k \notin \mathtt{Keys}\)
Cleanc(c):
  1. \(\textbf{return}\ c \in \{0,1\}^{*}\)

The box is transcribed from Küsters and Tuengerthal, Universally Composable Symmetric Encryption, ePrint 2009/055, revision 20090811:144642, Figure 10 (p. 27, the encryption clause, item 8) and Figure 12 (p. 29, the decryption clause, item 11). The source’s actual object, \(\mathcal{F}^{\mathsf{auth}}_{\mathsf{senc}}(q, L, (\mathcal{T}_{\mathsf{users}}, \mathcal{T}_{\mathsf{adv}}))\), is considerably larger than this box: three figures and thirteen numbered clauses (Figures 10–12, pp. 27–29), because it also handles long-term keys and public keys by delegating to two sibling functionalities, and lets messages carry embedded pointers to other keys so that key material itself can be sent as a plaintext.

This box keeps only the short-term-symmetric-key core — KeyGen, Store, Enc, Dec (items 2–4, 6, 8, 11 of the source) — and drops three things the source’s full object does, each stated here rather than left to be discovered by comparison:

  • No long-term-key or public-key delegation (the source’s items 9, 10, 12, 13). Those clauses do nothing this box’s own logic doesn’t already do once — they just forward the same encrypt/decrypt decision to a long-term-key or public-key sibling functionality and relay its answer. A page about the composed system that actually uses those siblings is where that forwarding belongs, not a box about what symmetric encryption alone guarantees.
  • No key-carrying plaintexts. The source lets a message contain (Key, ptr) tokens that get translated to the underlying key bits before encrypting and back to fresh pointers after decrypting, so that a protocol can transport key material as ordinary plaintext. This box treats every message as an opaque bit string; a page about key-encapsulation is where that machinery belongs.
  • No adversary-supplied algorithm pair. The source’s enc/dec are algorithms the adversary installs once (its item 1, Algorithms) and the functionality re-invokes on every call, so that one functionality can stay agnostic across whichever scheme eventually realizes it. A box that only ever means symmetric encryption has nothing else to stay agnostic across, so Enc/Dec here just ask the adversary directly for a ciphertext or a plaintext — the same behaviour with one fewer moving part, exactly the simplification already made on F-MAC.

Known realizations

Realized, Section 5.2 (protocol \(\mathcal{P}_{\mathsf{senc}}\), Figure 13, p. 33 of the same paper), by any IND-CPA and INT-CTXT secure (i.e. authenticated) encryption scheme, restricted to environments that avoid key cycles and the commitment problem. The paper also gives a separate, weaker variant, \(\mathcal{F}^{\mathsf{unauth}}_{\mathsf{senc}}\) (Section 6.1), which drops this box’s refusal of ill-formed or dishonestly-produced ciphertexts under an unknown key — decrypting them for real instead — realized from IND-CCA security alone, without requiring authentication.

Properties

  • Indistinguishability under an unknown key. Encrypting under a key the simulator does not hold discloses only \(L(\mathit{msg})\), never the message itself — the adversary’s answer to Enc is never given more than the leakage.
  • Ciphertext integrity under an unknown key. Dec recovers a plaintext for ciphertext \(c\) only if \(c\) is exactly what some prior Enc call under that same key produced; every other ciphertext, including an adversarially forged one, is refused. This is the box’s authenticated-encryption guarantee, and it is why \(\mathcal{F}^{\mathsf{unauth}}_{\mathsf{senc}}\) above needed a different name rather than a parameter.
  • Real crypto under a known key. Once a key is known — corrupted, or explicitly Stored by a party that already had it — both Enc and Dec simply defer to the adversary, which is exactly the standard real-vs-ideal contract: idealization applies only where the environment cannot already see through it.

Formal artifacts

No machine-checked formalization yet.

References:

  • Küsters and Tuengerthal. Universally composable symmetric encryption. In IEEE Computer Security Foundations Symposium (CSF), pages 293–307, 2009. Figure 10, p. 27 (item 8) and Figure 12, p. 29 (item 11), of revision 20090811:144642, the definition transcribed above.