15.1 Functionality

\(\Fsig \) below idealizes digital signatures, in the tradition of Canetti’s own ideal signature functionality [6]. Its process id is a parameter and not a constant. The name component is fixed — that is what the subscript records, by the naming convention of Chapter 1 — but the session and instance are not, so one system may hold a copy per session and several within a session, the situation composition exists to handle, and one Definition 1.2 would forbid outright if the whole process id were pinned. The code below reads neither component, so Chapter 7 lets it be read at any other — for an \(\admits \) meeting the condition of Definition 7.2, which any global or purely local one does. Recall from Section 3.4 that \(\Adv (x)\) abbreviates a call to the adversary on behalf of the party being served; in the ideal execution the simulator answers those calls, and every one of them here is sanitized in the sense of Chapter 12 before use.

How we write ideal functionalities.  The style is the same throughout. Wherever a value has to be produced and the specification does not pin it down, we let the simulator choose it and sanitize the choice on the fly. The simulator is then meant to have as much freedom as the security goal permits and no more — a design intention, not a theorem — and the goal stays visible in the predicates rather than buried in the code.

In \(\Fsig \) this happens three times, and the first two protect correctness. The operation \(\opl {Gen}\) takes the verification key from the adversary, and \(\Clean _{\vk }\) makes it an actual key, distinct from every key already issued and free of any signature already recorded valid under it, so generation always succeeds and keys neither collide nor arrive pre-forged. The operation \(\opl {Sign}\) takes the signature, and \(\Clean _{\sigma }\) makes it an actual signature not already recorded invalid, so signing succeeds whenever a key has been generated, and what it produces verifies. Locality asks for that, and asks in addition that the simulator answer without passing the token elsewhere, a condition on the simulator class rather than a property of the code. The operation \(\opl {Verify}\) is sanitized for unforgeability instead: a verdict outside \(\{0,1\}\) becomes \(0\), and so does any verdict of \(1\) on a fresh triple under a key an honest party generated, which makes signatures strongly unforgeable. There the good value is unique, so the sanitization is written inline rather than through \(\San \). Verification keys are not assumed authenticated, so \(\op {Verify}\) takes a \(\vk \) of its own.

\(\op {Leak}\), which Section 3.2 requires of an ideal functionality, hands the adversary the party’s verification key together with the signatures recorded valid under it, and nothing else of the state. The operation \(\op {Initialize}\) fixes the two tables and their types: \(\V {VK}\) holds one key per served party and \(\V {Ver}\) the verdict on each triple of key, message and signature, both starting everywhere at \(\unset \), the value that separates “not yet decided” from a recorded \(0\) or \(1\). Both \(\Keys \) and \(\Sigs \) are infinite and contain neither \(\none \) nor \(\unset \): infinite so that the sanitizers never run out of good values, and clean of the two markers so that membership already refuses them.

Where locality is wanted, the simulator class must be restricted to the responsive ones: those answering each simulator call without placing any call of their own, so the token returns at once and simulator calls are subroutine rather than coroutine calls — the discipline Chapter 9 enforces in code. For non-interactive, stateless signatures this costs nothing, the usual simulators being responsive already.

One further line in \(\op {Gen}\) and \(\op {Verify}\) guards against re-entrance. Section 3.6 lets a suspended instance be re-entered, and both operations suspend at an adversary call between testing a table entry and writing it; each therefore re-tests the entry on resumption, and a value recorded meanwhile wins. Without the re-test two nested calls could issue two keys to one party, or return different verdicts on one triple — the very consistency \(\V {Ver}\) exists to record.