F-MAC — Message authentication code

F-MAC (Message authentication code) 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 — no key at that pointer, or a key-guess it refuses. Every key is a bit string in one shared pool \(\mathtt{Keys}\); a party never holds a key directly, only a numbered pointer into its own \(\mathtt{Key}\) table. \(\mathtt{Known}\) tracks which keys the simulator already has real access to — either because it chose one at generation, or because some party Stored a bit string it already possessed — and is exactly the boundary between the functionality computing a tag for real and the functionality only remembering that it did.

Functionality \(\mathcal{F}_{\mathsf{MAC}}\)

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

Initialize():

1. \(\mathtt{Keys}, \mathtt{Known} \gets \varnothing\)
2. \(\mathtt{Key} : \mathcal{F}_{\mathsf{MAC}}.\mathbf{P} \times \mathbb{N} \rightharpoonup \mathtt{Keys}\)
3. \(\mathtt{Next} : \mathcal{F}_{\mathsf{MAC}}.\mathbf{P} \to \mathbb{N}\)
4. \(\mathtt{Next}[*] \gets 0\)
5. \(\mathtt{Tagged} : \mathtt{Keys} \to 2^{\mathcal{M}}\)
6. \(\mathtt{Tagged}[*] \gets \varnothing\)
7. \(\mathtt{Ver} : \mathcal{K} \times \mathcal{M} \times \Sigma \to \{0,1\} \cup \{\square\}\)
8. \(\mathtt{Ver}[*,*,*] \gets \square\)

id.KeyGen()from id′

9. \((\mathit{corr}, k) \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{KeyGen}\bigr)\)
10. \(k \gets \mathsf{San}[\mathsf{Clean}_{k}](k; \mathtt{Keys})\)
11. \(\mathtt{Keys} \gets \mathtt{Keys} \cup \{k\}\)
12. \(\textbf{if}\ \mathit{corr} = 1\ \textbf{then}\)
13. \(\mathtt{Known} \gets \mathtt{Known} \cup \{k\}\)
14. \(\mathit{ptr} \gets \mathtt{Next}[\mathit{id}.P]\);  \(\mathtt{Next}[\mathit{id}.P] \gets \mathit{ptr} + 1\)
15. \(\mathtt{Key}[\mathit{id}.P, \mathit{ptr}] \gets k\)
16. \(\textbf{return}\ \mathit{ptr}\)

id.Store(k)from id′

17. \(\textbf{if}\ k \in \mathtt{Keys} \setminus \mathtt{Known}\ \textbf{then}\)
18. \(\textbf{return}\ \bot\)// a bare guess of an unknown key is refused
19. \(\mathtt{Keys} \gets \mathtt{Keys} \cup \{k\}\);  \(\mathtt{Known} \gets \mathtt{Known} \cup \{k\}\)
20. \(\mathit{ptr} \gets \mathtt{Next}[\mathit{id}.P]\);  \(\mathtt{Next}[\mathit{id}.P] \gets \mathit{ptr} + 1\)
21. \(\mathtt{Key}[\mathit{id}.P, \mathit{ptr}] \gets k\)
22. \(\textbf{return}\ \mathit{ptr}\)

id.Mac(ptr, msg)from id′

23. \(k \gets \mathtt{Key}[\mathit{id}.P, \mathit{ptr}]\)
24. \(\textbf{if}\ k = \square\ \textbf{then}\)
25. \(\textbf{return}\ \bot\)
26. \(\sigma \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Mac}, \mathit{msg}\bigr)\)
27. \(\sigma \gets \mathsf{San}[\mathsf{Clean}_{\sigma}](\sigma)\)
28. \(\textbf{if}\ k \notin \mathtt{Known}\ \textbf{then}\)
29. \(\mathtt{Tagged}[k] \gets \mathtt{Tagged}[k] \cup \{\mathit{msg}\}\)
30. \(\textbf{return}\ \sigma\)

id.Verify(ptr, msg, σ)from id′

31. \(k \gets \mathtt{Key}[\mathit{id}.P, \mathit{ptr}]\)
32. \(\textbf{if}\ k = \square\ \textbf{then}\)
33. \(\textbf{return}\ \bot\)
34. \(\textbf{if}\ \mathtt{Ver}[k, \mathit{msg}, \sigma] \neq \square\ \textbf{then}\)
35. \(\textbf{return}\ \mathtt{Ver}[k, \mathit{msg}, \sigma]\)
36. \(b \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Verify}, \mathit{msg}, \sigma\bigr)\)
37. \(\textbf{if}\ b \not\in \{0,1\}\ \textbf{then}\)
38. \(b \gets 0\)
39. \(\textbf{if}\ k \notin \mathtt{Known} \wedge \mathit{msg} \notin \mathtt{Tagged}[k]\ \textbf{then}\)
40. \(b \gets 0\)// no forgery under an unknown key
41. \(\mathtt{Ver}[k, \mathit{msg}, \sigma] \gets b\)
42. \(\textbf{return}\ b\)

id.Leak()from id′

43. \(\textbf{return}\ \bigl(\{(\mathit{ptr}, \mathtt{Key}[\mathit{id}.P, \mathit{ptr}])\}_{\mathit{ptr} < \mathtt{Next}[\mathit{id}.P]}, \{(k, \mathtt{Tagged}[k]) : \exists\, \mathit{ptr}\, .\ \mathtt{Key}[\mathit{id}.P,\mathit{ptr}] = k\}\bigr)\)

Clean_k(k; Keys):

44. \(\textbf{return}\ k \in \{0,1\}^{*} \ \wedge\ k \notin \mathtt{Keys}\)

Clean_σ(σ):

45. \(\textbf{return}\ \sigma \in \Sigma\)

The box is transcribed from Küsters and Tuengerthal, Ideal key derivation and encryption in simulation-based security, ePrint 2010/295, revision 20101011:201701, Figure 6, p. 32 — the Mac and MacVerify clauses (items 13–14) of their single functionality \(\mathcal{F}_{\mathsf{crypto}}\), which also covers encryption, signatures and key derivation in one object parameterized over every key type at once (F-KDF draws on item 12 of the same figure). This box keeps only the MAC-relevant fragment: KeyGen/Store are the paper’s generic key-management commands restricted to this box’s one key type, and Mac/Verify are its items 13 and 14 in substance.

Two things the source does that this box doesn’t, both because a box that only ever stands for a MAC has less to stay generic across. The paper lets the adversary supply an arbitrary pair of algorithms, mac and mac-verify, and recomputes both fresh on every call, since \(\mathcal{F}_{\mathsf{crypto}}\) has to stay agnostic across whichever scheme eventually realizes it — here Mac and Verify just ask the adversary directly for a tag or a verdict, which is the same behaviour (the adversary still controls what “real” MACing and verifying compute) with one fewer moving part. And the paper’s forgery-prevention rule is stated in terms of mac-verify returning true on a message that was never MACed; here it is stated directly against the Tagged ledger, which is what that rule actually tracks.

Known realizations

Realized, Section 3.2 (p. 10 of the same paper), by protocol \(\mathcal{P}_{\mathsf{crypto}}\): it computes Mac and Verify for real using any UF-CMA-secure MAC scheme, which is exactly what the paper’s realization theorem requires.

Properties

• Unforgeability. Verify accepts a pair \((\mathit{msg},\sigma)\) under an unknown key only if that exact message was Maced under that key beforehand — a guarantee that holds with probability exactly 1 in the ideal world, and is what a UF-CMA realization is required to preserve.
• No confidentiality claim. The box authenticates; it discloses nothing about a MACed message beyond what Leak already reveals to a corrupted holder of the key. Realizing it does not require the underlying primitive to hide anything, only to resist forgery.

Formal artifacts

No machine-checked formalization yet.

References:

• Küsters and Tuengerthal. Ideal key derivation and encryption in simulation-based security. In Topics in Cryptology – CT-RSA 2011, volume 6558 of LNCS, pages 161–179, 2011. Figure 6, p. 32 of revision 20101011:201701, items 13–14, the definition transcribed above.