F-SIG — Digital signature

F-SIG (Digital signature) is part of Public-Key Primitives, Key Exchange, Messaging in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

Canetti’s ideal signature functionality: a local, per-party functionality that generates a key on first use, signs on request, and verifies — with the simulator given just enough freedom to choose the key and each signature, and no more, so that the guarantees below fall out of the code rather than needing to be argued separately.

Functionality

Reading the box: \(\mathcal{A}(\cdot)\) is a call to whichever adversary or simulator occupies the slot, answered by the simulator in the ideal execution; \(\mathsf{San}[\mathsf{Clean}](\cdot)\) resamples until the named predicate holds, with \(\mathsf{Clean}_{\mathit{vk}}\) and \(\mathsf{Clean}_{\sigma}\) spelled out at the end of the box; \(\mathbf{C}\) is the set of corrupted parties; \(\mathcal{K}\), \(\mathcal{M}\), \(\Sigma\) are the key, message and signature spaces, all infinite and containing neither \(\bot\) nor \(\square\), so a sanitizer never runs out of good values and membership alone refuses the two markers. The header line fixes the process id, the served parties \(\mathbf{P}\), the admitted callers \(\mathbf{N}\), the used slots \(\mathbf{U}\) (the adversary, at every party served) and the parameters \(\mathit{par}\); the process id is a parameter rather than a constant, so a system may hold one copy per session and several within a session.

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

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

Initialize():

\(\mathtt{VK} : \mathcal{F}_{\mathsf{Sig}}.\mathbf{P} \to \mathcal{K} \cup \{\square\}\)
\(\mathtt{VK}[*] \gets \square\)
\(\mathtt{Ver} : \mathcal{K} \times \mathcal{M} \times \Sigma \to \{0,1\} \cup \{\square\}\)
\(\mathtt{Ver}[*,*,*] \gets \square\)

id.Gen()from id′

\(\textbf{if}\ \mathtt{VK}[\mathit{id}.P] \neq \square\ \textbf{then}\)
\(\textbf{return}\ \mathtt{VK}[\mathit{id}.P]\)
\(\mathit{vk} \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Gen}\bigr)\)
\(\textbf{if}\ \mathtt{VK}[\mathit{id}.P] \neq \square\ \textbf{then}\)
\(\textbf{return}\ \mathtt{VK}[\mathit{id}.P]\)// recorded while suspended
\(\mathit{vk} \gets \mathsf{San}[\mathsf{Clean}_{\mathit{vk}}](\mathit{vk}; \mathtt{VK}, \mathtt{Ver})\)
\(\mathtt{VK}[\mathit{id}.P] \gets \mathit{vk}\)
\(\textbf{return}\ \mathit{vk}\)

id.Sign(msg)from id′

\(\mathit{vk} \gets \mathtt{VK}[\mathit{id}.P]\)
\(\textbf{if}\ \mathit{vk} = \square\ \textbf{then}\)
\(\textbf{return}\ \bot\)
\(\sigma \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Sign}, \mathit{msg}\bigr)\)
\(\sigma \gets \mathsf{San}[\mathsf{Clean}_{\sigma}](\sigma; \mathit{msg}, \mathit{vk}, \mathtt{Ver})\)
\(\mathtt{Ver}[\mathit{vk}, \mathit{msg}, \sigma] \gets 1\)
\(\textbf{return}\ \sigma\)

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

\(\textbf{if}\ \mathtt{Ver}[\mathit{vk}, \mathit{msg}, \sigma] \neq \square\ \textbf{then}\)
\(\textbf{return}\ \mathtt{Ver}[\mathit{vk}, \mathit{msg}, \sigma]\)
\(b \gets \mathcal{A}\bigl(\mathit{id}.\mathsf{Verify}, \mathit{vk}, \mathit{msg}, \sigma\bigr)\)
\(\textbf{if}\ \mathtt{Ver}[\mathit{vk}, \mathit{msg}, \sigma] \neq \square\ \textbf{then}\)
\(\textbf{return}\ \mathtt{Ver}[\mathit{vk}, \mathit{msg}, \sigma]\)// recorded while suspended
\(\textbf{if}\ b \not\in \{0,1\}\ \textbf{then}\)
\(b \gets 0\)
\(\textbf{if}\ \exists\, P' \not\in \mathbf{C} \, : \, \mathit{vk} = \mathtt{VK}[P']\ \textbf{then}\)
\(b \gets 0\)// no forgery under an honest key
\(\mathtt{Ver}[\mathit{vk}, \mathit{msg}, \sigma] \gets b\)
\(\textbf{return}\ b\)

id.Leak()from id′

\(\textbf{if}\ \mathtt{VK}[\mathit{id}.P] = \square\ \textbf{then}\)
\(\textbf{return}\ (\bot, \varnothing)\)
\(\textbf{return}\ \bigl(\mathtt{VK}[\mathit{id}.P], \{\, (\mathit{msg},\sigma) : \mathtt{Ver}[\mathtt{VK}[\mathit{id}.P],\mathit{msg},\sigma] = 1 \,\}\bigr)\)

Clean_vk(vk; VK, Ver):

\(\textbf{return}\ \mathit{vk} \in \mathcal{K} \ \wedge\ \neg\exists\, P : \mathtt{VK}[P] = \mathit{vk}\)
\(\wedge\ \neg\exists\, \mathit{msg},\sigma : \mathtt{Ver}[\mathit{vk},\mathit{msg},\sigma] = 1\)

Clean_σ(σ; msg, vk, Ver):

\(\textbf{return}\ \sigma \in \Sigma \wedge \mathtt{Ver}[\mathit{vk},\mathit{msg},\sigma] \neq 0\)

The box is transcribed from UC for Gamers (§15.1, p. 146), line numbering and all. Two tables carry all the state: \(\mathtt{VK}\), one verification key per served party, and \(\mathtt{Ver}\), every verification verdict decided so far. Both start everywhere at \(\square\), the marker that separates “not yet decided” from a recorded \(0\) or \(1\) — and it is that separation, not the verdicts themselves, that the operations are built around.

Where the code is doing more than it looks:

Gen lets the adversary choose the key (line 7) but not keep it: the choice passes through a sanitizer first (line 10). \(\mathsf{Clean}_{\mathit{vk}}\) demands an actual key, not one already issued to another party, and not one already recorded valid on some message — the last condition is the easy one to miss, and without it a simulator could hand an honest party a key under which a forgery had already been accepted.
Sign returns \(\bot\) for a party with no key (line 15) rather than quietly generating one. Its sanitizer only rules out a signature already recorded invalid on this exact triple; a repeat of an existing valid signature is fine, since recording it valid again changes nothing.
Verify is where unforgeability actually lives, in one line: an offered verdict is forced to \(0\) whenever \(\mathit{vk}\) belongs to some honest party (line 28). That is what makes the functionality unforgeable rather than merely “whatever the simulator says”. No “was it ever signed?” test is needed alongside it — a triple that was signed already carries the verdict \(1\) and returns at line 21, before the slot is ever consulted.
Leak gives up the party’s own key and every message/signature pair recorded valid under it, and nothing else of the state. In particular a corrupt party learns no verdict recorded under anyone else’s key.

Two further lines exist only to guard against re-entrance: a suspended instance may be re-entered between the test of a table entry and the write to it, so Gen (line 8) and Verify (line 23) re-test on resumption and a value recorded meanwhile wins. Without them two nested calls could issue two keys to one party, or return different verdicts on one triple — the very consistency \(\mathtt{Ver}\) exists to record. Locality of Gen and Sign additionally asks that the simulator answer without passing the token elsewhere: a restriction to responsive simulators, which costs nothing for non-interactive, stateless signatures.

Known realizations

Realized, up to the ordinary reduction loss of the underlying primitive, by any EUF-CMA-secure signature scheme run over local randomness and storage (see F-Rand and F-Store): the scheme’s own key-generation, signing, and verification algorithms, with coins drawn and erased through F-Rand and the key pair held in F-Store. Correctness of the scheme gives correctness of the simulation; strong unforgeability under chosen-message attack gives the functionality’s unforgeability, up to the scheme’s own advantage bound.

Verification keys are deliberately not assumed authenticated on their own (Verify takes a \(\mathsf{vk}\) of its own, unconnected to any caller) — binding a key to the party that owns it is G-PKI’s job, not this functionality’s.

Properties

Both proven with probability exactly \(0\) against every occupant of the adversary slot:

Correctness. A signature honestly produced by Sign always verifies (there is no environment/adversary pair that can make an honestly-signed message/signature pair fail Verify).
Unforgeability, and strong unforgeability at that: no environment/adversary pair can make Verify accept a fresh triple — not just a fresh message, but a triple that wasn’t itself the direct output of a Sign call — under an honest party’s key.

A further, more surprising pair of results (from the same source’s deeper treatment): these two properties do not by themselves characterize the functionality — a variant that memoizes nothing about repeated verification queries satisfies both yet is distinguishable from this one — but four properties together (correctness, unforgeability, plus verification-consistency across repeated queries and one-key-per-party) do characterize it exactly. And realizations can be strictly stronger than the ideal object they realize: a concrete scheme-backed realization can be collision-resistant (no honest key ever verifies one signature under two distinct messages) even though F-Sig itself, as specified above, provably is not.

Formal artifacts

No machine-checked formalization yet.

References:

Canetti. Universally composable signature, certification, and authentication. In 17th IEEE Computer Security Foundations Workshop (CSFW), pages 219–233, 2004.
Backes and Hofheinz. How to break and repair a universally composable signature functionality. In Information Security Conference (ISC), 2004.
Küsters and Tuengerthal. Joint state theorems for public-key encryption and digital signature functionalities with local computation. In 21st IEEE Computer Security Foundations Symposium (CSF), pages 270–284, 2008.
UC for Gamers, this site’s own book draft on composable security. Chapter “Digital Signatures” gives the functionality above and both properties in full; the deep-dive chapter “F-Sig: A Deeper Dive” gives the characterization and collision-resistance results.