Definition 5.1 is a shape, and a shape is worth an instance. We give one game \(\Gm \) over \(\Fsig \) carrying two properties: \(\opl {FinCor}\), saying that what the signing interface produces verifies, and \(\opl {FinUF}\), saying that nothing else does. They are two finalizations of one shell rather than two games, which is what the shape now allows and what these two ask for — they read the same trace, of the same oracles, and differ in the verdict alone. The environment chooses which it is judged on by choosing which to call, and calling one closes the game against the other.
Both take the search reading of Definition 5.8,
because winning either is meant to be impossible and not merely no better than a coin: a signature scheme whose forgeries succeed half the time is broken, not average.
They are played over the game system \(\gamma := \{\Gm \} \cup \{\Fsig \}\), with \(\Fsig .\admits := \{\Gm .\PID \}\) — the game’s process id, pinned, not its name — and \(\Fsig .\Ps \subseteq \Gm .\Ps \), so the relays exist at every party \(\Fsig \) serves and, at the root, address a party it does not serve and are answered \(\rej \) at line 1 — the root being where the game finalizes, not where it plays. Inside an interface at \(\id \) we write \(\id _{\Fsig }\) for \((\Fsig .\PID ,\id .P)\), the interface of \(\Fsig \) at the party the game was called at. That is tightness at \(\{\Gm \}\), which Definition 5.1 requires, and here it earns its keep twice over. It makes \(\gamma \) a legal game system; and it makes the trace complete. No caller but \(\Gm \) passes line 2 at \(\Fsig \): not the environment, whose \(Z\)-identities and fresh names lie outside a pinned \(\admits \); not the adversary, whose claim is an \(A\)-identity; and not a machine the environment hosts at an invented instance of the game’s name, which is what pinning the id rather than the name refuses. So every signature \(\Fsig \) ever issues passes through line 8 below and is recorded. A game whose verdict is “this was not obtained from the signing interface” has no other way to know.
Game shell over \(\Fsig \); the finalizations follow
\(\PID := (\Gm .F,0,0)\), \(\Ps := \Fsig .\Ps \cup \{Z\}\), \(\admits := \Zpid \), \(\uses := \{(\Fsig ,\serves _{\Gm })\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\opdef {Gen}()\) from \(\id '\)
\(\id .\opdef {Sign}(\msg )\) from \(\id '\)
auto
\(\id .\opdef {Verify}(\vk ,\msg ,\sigma )\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
The finalizations of \(\Gm \); the shell over \(\Fsig \) is shared
\(\id .\opdef {FinCor}()\) from \(\id '\) (correctness)
\(\id .\opdef {FinUF}()\) from \(\id '\) (unforgeability)
Four things about the code. The trace is a sequence, \(\in \) means occurrence in it, and no verdict reads the order. The verdicts read \(\V {tr}\) and the register and call nothing, which is why the root exemption in \(\serves _{\Gm }\) suffices and \(\Fsig \) need not serve \(Z\). Both ask \(P \notin \Cs \) at the end rather than at the time of signing, and monotonicity (Section 3.5) makes that the stronger reading: a party honest when the game closes was honest throughout. Correctness asks \(\sigma \in \Sigs \) because \(\op {Sign}\) answers \(\none \) where no key has been generated, and \(\none \) is no signature to hold against the functionality. And unforgeability is strong: line 28 excludes the triple, not the message, so a second signature on a signed message counts as a forgery — which is the notion Chapter 15’s sanitizer was written to give.
Proposition 15.1 (\(\Fsig \) has both properties). For \(\op {Fin}\) either of \(\op {FinCor}\) and \(\op {FinUF}\), for every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {Fin}}] = 0\). So \(\{\Fsig \}\) has each property within \(0\) against \(\bigl (\ZenvSet _{\gamma ,\gamma },\Xset \bigr )\) in the sense of Definition 5.8, for \(\Xset \) the class of all occupants.
Proof. One preliminary and two verdicts. The preliminary is that both parties named by a verdict must be honest, and it is not bookkeeping: at a corrupt party the core does not run and the answer is the adversary’s, so a mediated \(\op {Verify}\) could report a \(0\) on a good signature or a \(1\) on a forgery, and either finalization would fire with \(\Fsig \) having done nothing wrong. Correctness then follows from \(\op {Sign}\) recording \(\V {Ver}[\vk ,\msg ,\sigma ] \gets 1\) and \(\op {Verify}\) returning a recorded entry at its first line. Unforgeability splits on whether \(\op {Verify}\) read an entry or computed one: it cannot have computed a \(1\) under an honest party’s key, so the entry was recorded, and only \(\op {Sign}\) records one. Take parties honest at the close. Monotonicity makes them honest throughout, so no call the game places at them is mediated, line 4 firing only at a corrupt party and the game’s own name lying in \(\bits \). Both verdicts ask this of the signer \(P\) and of the verifier \(Q\), and both need it of both: at a corrupt party the core does not run and the answer is the adversary’s, so a mediated \(\op {Verify}\) reports whatever it likes — a \(0\) on a good signature, or a \(1\) on a forgery — and either finalization would return \(1\) with \(\Fsig \) having done nothing wrong.
For correctness, suppose \((\atom {sign},P,\msg ,\sigma ) \in \V {tr}\) with \(\sigma \in \Sigs \). The core of \(\op {Sign}\) ran, so it sanitized \(\sigma \) against \(\Clean _{\sigma }\) and then set \(\V {Ver}[\vk ,\msg ,\sigma ] \gets 1\) for \(\vk = \V {VK}[P]\), which \(\op {Gen}\) fixed once and never changes. Any later \(\op {Verify}(\vk ,\msg ,\sigma )\) finds that entry set and returns it at its first line, so it returns \(1\); thus \((\atom {ver},Q,\vk ,\msg ,\sigma ,0) \notin \V {tr}\) for every \(Q\), and line 20 gives \(0\).
For unforgeability, suppose \((\atom {ver},Q,\vk ,\msg ,\sigma ,1) \in \V {tr}\) with \(\vk = \V {VK}[P]\) for an honest \(P\). Either \(\op {Verify}\) read a recorded entry or it computed one. It cannot have computed a \(1\): the last test before writing \(\V {Ver}\) sets \(b \gets 0\) whenever \(\vk = \V {VK}[P']\) for some \(P' \notin \Cs \), which \(P\) witnesses. So the entry was recorded, and only \(\op {Sign}\) records a \(1\) — at the party whose key is \(\vk \), that party being \(P\) since \(\Clean _{\vk }\) issues no key twice. Hence \((\atom {sign},P,\msg ,\sigma ) \in \V {tr}\) and line 28 gives \(0\). □
The bound is not the interesting part; that it is \(0\) merely says the ideal functionality was written to have these properties, as an ideal functionality should be. The content is what Corollary 5.11 then does with it, and the search reading is what makes that useful: a system \(\pi \) put in place of \(\{\Fsig \}\) wins either finalization with probability at most \(\varepsilon \), against every adversary and not only the dummy, and under the search reading that probability is the advantage, so \(\varepsilon \) bounds the property itself. Had the decision reading been taken the same conclusion would read \(2\varepsilon \) on \(2\Pr [\Win _{\op {Fin}}]-1\), which for a game meant to be unwinnable is no constraint at all — a forger succeeding half the time meets it. That is the calibration rule of Chapter 5 applied where it bites, and why Proposition 5.10 carries both displays: each finalization inherits at the scale its own reading fixes, and these two inherit at \(\varepsilon \).
Four conditions come with the corollary and none is discharged by emulation alone. The replacement of \(\{\Fsig \}\) by \(\pi \) must be well-formed; \(\{\Gm \} \cup \pi \) must again be a game system, which asks \(\pi \)’s members to pin \(\Gm .\PID \) where \(\Fsig \) did, since tightness is part of Definition 5.1; the simulator and the adversary must be refusal-oblivious; and the environments must silence no \(Z\)-identity. A realization is thus never separately argued to be correct or unforgeable — it inherits both from the one emulation proof, together with those four checks, and the two finalizations above are what the inheritance is of .
One caveat travels with it, and this is where it bites. Corollary 5.11 asks that the cores of the game system place no responsive call, and \(\Fsig \) as written reaches the slot through \(\Adv (\cdot )\), so the corollary applies. Should one adopt Chapter 9’s advice and write \(\Adv ^{!}\) in \(\op {Gen}\), \(\op {Sign}\) and \(\op {Verify}\) — which buys locality — the transfer must be argued directly instead, for the reason Remark 9.4 gives. Locality and inheritance are, as things stand, priced against each other.