Proposition 21.1 runs from a scheme to the properties. The converse would run the other way and much further: that the two properties characterize \(\Fsig \), so that any functionality carrying its interfaces and satisfying them realizes it. It is a natural conjecture — properties are what we ask of an ideal object, so an object satisfying them ought to be as good as the one we asked them of — and it is false.
Proposition 21.2 (The two properties do not characterize \(\Fsig \)). There is a standard functionality \(\F '\) with \(\Fsig \)’s fields and interfaces, having both \(\opl {FinCor}\) and \(\op {FinUF}\) within \(0\) against every environment and every occupant of the slot, such that \(\{\F '\}\) does not UC-emulate \(\{\Fsig \}\) within any \(\varepsilon < \tfrac 12\).
Proof. Let \(\F '\) be \(\Fsig \) with one change: in \(\op {Verify}\), when no honest party’s key equals the queried \(\vk \) — that is, when \(\vk \neq \V {VK}[P']\) for every \(P' \notin \Cs \) — the answer is a fresh uniform bit, recorded nowhere, so that a later query on the same triple is answered independently. On every other triple \(\F '\) is \(\Fsig \) exactly, memoization included.
\(\F '\) has both properties within \(0\). Each of lines 20 and 28 is existential over a \((\atom {gen},P,\vk )\) entry with \(P \notin \Cs \), so a triple whose \(\vk \) is no honest party’s key witnesses neither, and on all other triples \(\F '\) answers as \(\Fsig \) does, whose verdicts are \(0\) by Proposition 15.1.
It does not emulate. Let \(\Zenv \) pick any \(\vk ^{*}\), \(\msg \), \(\sigma \) with \(\vk ^{*}\) generated by nobody, corrupt no one, and call \(\op {Verify}(\vk ^{*},\msg ,\sigma )\) twice at an honest party, returning \(1\) if the two answers differ. Against \(\F '\) the answers are independent uniform bits, so it returns \(1\) with probability \(\tfrac 12\). Against \(\Fsig \) the first call fixes \(\V {Ver}[\vk ^{*},\msg ,\sigma ]\) and the second returns it, so the answers agree and it returns \(1\) with probability \(0\) — whatever the simulator does, the memoization being \(\Fsig \)’s own code and no value of the slot’s able to unfix it. The advantage is \(\tfrac 12\). □
The diagnosis is more useful than the counterexample. Emulation pins an object’s whole observable behaviour; the two properties pin two things about it — that honestly produced signatures verify, and that forgeries under honest keys do not. Everything else is out of their reach, and the gap has a shape: both verdicts are existential over \((\atom {gen},P,\vk )\) with \(P\) honest, so nothing whatever is said about keys no honest party generated, and nothing is said about consistency, one answer being all either verdict inspects. What is missing is not a stronger notion of unforgeability but two further properties, and they are the ones \(\Fsig \)’s code makes obvious once looked for: its \(\op {Verify}\) memoizes, and its \(\op {Gen}\) issues one key per party.
Two further finalizations of the shell of Section 15.2
\(\id .\opdef {FinCons}()\) from \(\id '\) (consistency)
\(\id .\opdef {FinOne}()\) from \(\id '\) (one key per party)
Both take the search reading, both are attained at \(0\) by \(\Fsig \) — \(\opl {FinCons}\) because \(\V {Ver}\) is written once per triple and read thereafter, \(\opl {FinOne}\) because \(\V {VK}[P]\) is written once and read thereafter, each by the same first-write-wins argument Proposition 16.1 makes for the directory — and both are attained at \(0\) by \(\psig \), by \(\op {Ver}\)’s determinism and \(\Fstore \)’s \(\op {FinKeep}\) respectively. Neither asks anything of a corrupt party: \(\op {FinCons}\) names no party at all, the game’s own wrapper having already kept corrupt answers out of \(\V {tr}\).
Theorem 21.3 (The converse, from the four properties). Let \(\F '\) be a standard functionality with \(\Fsig \)’s fields and interfaces, whose \(\op {Sign}\) returns \(\none \) exactly when no key has been generated at the calling party, and let \(\F '\) have \(\op {FinCor}\), \(\op {FinUF}\), \(\op {FinCons}\) and \(\op {FinOne}\) within \(0\) against \(\ZenvSet _{\gamma ,\gamma }\) and every occupant of the slot, for \(\gamma \) the game system of Section 15.2 with \(\F '\) in place of \(\Fsig \). Then \(\{\F '\}\) UC-emulates \(\{\Fsig \}\) within \(0\): for every occupant \(\Adv \) there is a simulator \(\Sim _{\Adv }\) with
for every \(\Zenv \in \ZenvSet _{\{\F '\},\{\Fsig \}}\).
Proof. The simulator is the obvious one — \(\Adv \) bundled with an internal copy of \(\F '\), answering each of \(\Fsig \)’s three slot queries by putting the same call to that copy — so the whole of the argument is that the two sides never disagree on a returned value. Since \(\Fsig \)’s answer is the slot’s answer unless its own code overrides, that reduces to showing no override ever fires, and there are exactly four: \(\op {Gen}\)’s memoization, \(\op {Gen}\)’s sanitizer, \(\op {Sign}\)’s sanitizer, and \(\op {Verify}\)’s honest-key test. Each is taken in turn and excluded by one of the four hypothesised properties at \(0\), the sanitizer cases splitting further by which repair the sanitizer would make. That is where all four properties are spent, and it is why the theorem needs exactly them. The simulator \(\Sim _{\Adv }\) bundles \(\Adv \) with an internal copy of \(\F '\) and runs it on the calls \(\Fsig \) reports. The functionality \(\Fsig \) asks the slot for exactly the three values it does not pin — the key at \(\op {Gen}\), the signature at \(\op {Sign}\), the bit at \(\op {Verify}\) — and \(\Sim _{\Adv }\) answers each by putting the same call to its internal \(\F '\) at the same identity and forwarding what comes back, letting the hosted \(\Adv \) see, and answer, whatever \(\F '\)’s own code would put to a slot. Leakage and corruption instructions it serves from the internal copy likewise; note that this is why \(\F '\)’s \(\opl {Leak}\) need not resemble \(\Fsig \)’s at all, the environment reaching it only through the slot, which \(\Sim _{\Adv }\) occupies.
Couple the two executions on equal tapes as in Lemma 11.2. Everything reduces to one claim: at every call, \(\Fsig \) returns what the internal \(\F '\) returned, so that the two sides agree on the value the environment sees. Since \(\Fsig \)’s answer is the slot’s answer unless its own code overrides, it is enough that no override ever fires, and there are exactly four.
\(\op {Gen}\)’s memoization and \(\op {Gen}\)’s sanitizer. If \(\V {VK}[\id .P]\) is already set \(\Fsig \) returns it; \(\op {FinOne}\) at \(0\) says the internal \(\F '\) returns the same key at that party too, so the two agree. Otherwise \(\San [\Clean _{\vk }]\) replaces the offered \(\vk \) if it is not a key, or duplicates one already issued, or has a signature already recorded valid under it. Not a key: then \(\F '\) answered \(\op {Gen}\) with a non-key, and a later \(\op {Sign}\) at that party would carry \(\sigma \in \Sigs \) with \((\atom {ver},\cdot ,\vk ,\cdot ,\cdot ,0)\) available to the environment — excluded by \(\op {FinCor}\) at \(0\) once the environment signs and verifies, which it may. Duplicate: two honest parties then share a key, and signing at one and verifying at the other wins \(\op {FinUF}\), excluded. Pre-signed: some \(\V {Ver}[\vk ,\msg ,\sigma ] = 1\) stands before \(\vk \) is issued, and \(\Fsig \) records a \(1\) only at \(\op {Sign}\), so an honest party signed under a key not yet generated — which \(\Fsig \)’s \(\op {Sign}\) refuses, returning \(\none \), and which the hypothesis on \(\F '\)’s \(\op {Sign}\) refuses too. So the sanitizer is idle.
\(\op {Sign}\)’s sanitizer. The sanitizer \(\San [\Clean _{\sigma }]\) replaces \(\sigma \) if it is not a signature or if \(\V {Ver}[\vk ,\msg ,\sigma ] = 0\) already. Not a signature: \(\op {FinCor}\)’s \(\sigma \in \Sigs \) conjunct is exactly the reading that lets this case be excluded, the environment verifying the returned value and \(\op {FinCor}\) forbidding a \(0\). Already \(0\): then the same triple verified \(0\) earlier and verifies \(1\) now — the internal \(\F '\) having produced a signature it must accept — which is \(\op {FinCons}\), excluded at \(0\). So it too is idle.
\(\op {Verify}\)’s memoization and its honest-key suppression. The first returns the recorded verdict where one exists, and \(\op {FinCons}\) at \(0\) says the internal \(\F '\) answers the same triple the same way, so they agree; this is the override the counterexample of Proposition 21.2 exploited, and it is exactly what \(\op {FinCons}\) closes. The second sets \(b \gets 0\) on a fresh triple under an honest party’s key, and \(\op {FinUF}\) at \(0\) says the internal \(\F '\) answers \(0\) there too — a \(1\) being its win condition. So both agree.
No override fires, every value the environment sees is the internal \(\F '\)’s own, and the coupled runs proceed in step to the same halt, exactly as in Lemma 11.2’s no-flag case. The distributions are equal and the advantage is \(0\). □
So the converse holds, and what it took to hold is the point. Two properties were not a characterization; four are, and the two added are not deep facts about signing but the two places \(\Fsig \)’s code commits — a table written once and read thereafter, twice over. A functionality’s properties characterize it exactly when they cover every such commitment, and reading a specification for its commitments is a better way to find the missing property than asking what else one would like to be true.