Chapter 11
Identical Until Bad
Code-based proofs advance by hops [5, 13]: two games that are the same program except where a flag has been raised, and a bound on the probability of the raising. The fundamental lemma of game playing is the licence — if the games are identical until \(\V {bad}\), their outcomes differ with probability at most \(\Pr [\Bad ]\) — and its proof is a coupling: run both games on the same coins and they cannot part company before the flag goes up. In this paper a game is not one program. An execution runs an environment, a slot occupant, a register and a system; the token wanders among them; the occupant may be handed the token mid-operation and drive the rest of the execution before answering — the freedom Chapter 9 exists to discipline — and a hop must survive all of it. This chapter replays the lemma over executions, and the finding is that the wandering costs nothing: the lemma below has no hypothesis at all.
Where the flag lives. \(\V {bad}\) is an ordinary state variable of an ordinary machine: declared \(\V {bad} \gets \false \) in \(\op {Initialize}\), never assigned any value but \(\true \) afterwards, owned like the rest of a machine’s state by the machine that declares it. The framework already keeps every other hand off it — the one thing a machine can do to state it does not own is provoke calls that read or extend it, and at a corrupt party \(\opl {Mediate}\) replaces answers, never state (Remark 5.4) — so a flag is raised by its owner’s own code or not at all. Whether anyone may read it is immaterial, through an interface or through \(\op {Leak}\), which bypasses \(\opl {Guard}\): until the flag is raised the two machines below answer any read alike, and after it is raised the lemma has already paid. Several machines may carry flags at once — members sharing a name included, each owning its own — and \(\Bad \) below is the event that some machine raises some flag.
Definition 11.1 (Identical until bad). Standard functionalities \(\F \) and \(\F '\) are identical until bad if their five fields agree; their \(\op {Initialize}\)s agree line for line, declarations common to both sides and \(\V {bad} \gets \false \) among them; and their remaining code agrees except inside bad-guarded blocks, of two shapes: the continuation of an assignment \(\V {bad} \gets \true \), from just past the assignment to the end of its enclosing block — the branch, loop or operation body the assignment stands in, so that everything in the continuation is reached only across the assignment — and the body of a conditional whose test is \(\V {bad}\). Erasing the bad-guarded blocks from both sides leaves one functionality, operation for operation and line for line, \(\op {Leak}\) included; in particular the assignments themselves are common code, each heading its own divergent continuation, and neither side assigns \(\V {bad}\) any value but \(\true \). Equal functionalities are identical until bad, with nothing to erase. Two occupants of the adversary slot are identical until bad when their \(\op {Initialize}\)s and cores are, read the same way. Systems \(\pi \) and \(\pi '\) are identical until bad if some bijection pairs every member of one with a member of the other identical until bad with it.
Two things about the shape, both [5]’s. Membership is checked by inspection — it is a comparison of code, not a claim about behaviour — which is what keeps hops cheap to audit. And it is built so that a divergent statement cannot run early: the only ways into a bad-guarded block are its head, an assignment that raises the flag as it is crossed, and a test of the flag itself, and the flag is monotone — so nothing bad-guarded runs while its owner’s flag is down. Because paired members carry equal fields, the two systems occupy the same identities and use the same names, \(\ncl {\pi } = \ncl {\pi '}\), and one class of environments serves both: \(\ZenvSet _{\pi ,\pi '} = \ZenvSet _{\pi ,\pi } = \ZenvSet _{\pi ',\pi '}\).
Lemma 11.2 (The fundamental lemma, over systems). Let systems \(\pi \) and \(\pi '\) be identical until bad, let occupants \(\mathcal {X}\) and \(\mathcal {X}'\) of the adversary slot be identical until bad, and let \(\Zenv \in \ZenvSet _{\pi ,\pi '}\). Write \(\Bad \) for the event that some machine executes an assignment \(\V {bad} \gets \true \), in whichever execution is named. Then
and, writing \(\Pr [\Bad ]\) for the common value,
If moreover the two systems are game systems — the pairing then matches game to game, fields being preserved — the same holds of every finalization \(\op {Fin}\), which the two games share:
Proof. One coupling, read pointwise. Fixing every tape fixes both executions outright, so the two may be taken from one sample and compared step by step. The induction shows that while no flag is up the two correspond strictly and the token stands on common code — which is exactly what Definition 11.1’s two bad-guarded shapes buy, neither being reachable except across the assignment that raises the flag or through a test that fails while it is down. The first raising is therefore the same step on both sides, and that is the first display: \(\Pr [\Bad ]\) is one number rather than two that happen to share a bound. Off \(\Bad \) the two runs are equal outright, so every fact of the run has a single indicator there, and each difference of probabilities is at most the measure of the set where indicators may differ. Two conventions of Chapters 1 and 3.6 are used, the ones the absorption lemma restates: each machine draws from its own coin tape, uniform and independent of every other’s, read only when its code samples — an environment’s hosted copies keeping tapes of their own, bundling merging nothing — and \(\op {Initialize}\) places no calls. Fixing every tape therefore fixes an execution outright: which machine holds the token, at which line of which operation, with what state, and what its next statement does are functions of the configuration, coins entering only as the next unread positions of the holder’s own tape.
Couple the two executions. The pairing matches machine to machine — member to member, occupant to occupant, the environment and the register each to themselves — and paired machines occupy the same identities, so give paired machines equal tapes. Each execution separately keeps its distribution, tapes on either side being uniform and independent, so both may be read off one sample of tapes and compared pointwise. Say the two correspond strictly at a configuration if (C1)–(C4) of Definition 4.17 hold under the pairing — equal states, equal unread tapes, the token in paired hands at the same line with the same local values, suspended callers matching frame for frame — with no relay anywhere and nothing elided.
At the start they correspond strictly. Line 1 initialises the register and every member on both sides, in whatever order — \(\op {Initialize}\) places no calls and touches no state but its owner’s, so the order leaves no trace in the configuration; paired members run \(\op {Initialize}\)s that agree line for line, \(\V {bad} \gets \false \) among them, placing no calls and drawing, where they draw, the same positions of equal tapes; and line 2 hands both tokens to the one environment at the same identity.
Suppose the two correspond strictly, no flag yet raised on either side, and let one statement run. The token stands in paired machines at the same line, and that line is common code: a bad-guarded statement is reached only through its head or through a test of the flag, the head raises the flag as it is crossed, the test fails while the flag is down, and no flag is up. So the statement is the same statement, read over the same state and the same next coins, histories having consumed tape for tape alike. If it writes, both sides write alike; if it returns, both resume the same frame with the same value; if it places a call, both place the same call — target, payload and claimed identity — met by the same wrappers over equal fields and an equal register state, landing at paired machines, or at no machine and answered \(\rej \) alike; and every delivery Section 3.6 fixes — \(\rej \) for a refused require, \(\none \) where a core would return \(\rej \) or a mediated slot answers one — is a rule, not a choice. Strict correspondence survives the step. And if the statement is an assignment \(\V {bad} \gets \true \) — common code, standing at the head of its divergent continuation — both sides execute it, and the step is the first raising in both executions at once.
Pointwise on the coupled space, then: either no flag is ever raised and the two executions correspond strictly at every step — so one halts exactly when the other does, with the same output, the environment being one machine resumed alike — or there is a first raising, it is simultaneous, and the executions agree up to and through it. The event \(\Bad \) therefore has one indicator on the coupled space, which is the first display, with equality. Off \(\Bad \) the runs are equal outright, so any fact of the run has one indicator there too: the output, and, for game systems, the event \(\Win _{\op {Fin}}\) that the interface \((\Gm .\PID ,Z).\fopl {Fin}\) returns \(1\) (Definition 5.8). Each difference of probabilities is at most the measure of the set where its indicators may differ, which is \(\Pr [\Bad ]\). □
The definition and the proof have a picture each, and they are worth seeing together, since one is exactly what the other consumes. Above is what Definition 11.1 asks of the code; below is what the coupling then does with it. Neither panel uses the box-and-wire vocabulary of the earlier figures, and that is the point: nothing here is moved from one machine to another, so there is nothing to draw a wire between.
![[Picture]](main8x.svg)
Figure 6: Identical until bad, in two panels. Above, what Definition 11.1 asks of the code; below, what the coupling does with it. Neither panel uses the box-and-wire vocabulary of the earlier figures, because nothing here moves from one machine to another. (Definition 11.1 and Lemma 11.2.)
The upper panel is checkable by inspection, which is what keeps a hop cheap to audit: it is a comparison of code, not a claim about behaviour. The two shaded shapes are the only ones allowed, and between them they are why nothing shaded can run while the flag is down — the only ways in are the head, which raises the flag as it is crossed, and a test of the flag, which fails while it is down. So the shading above is exactly what runs beyond the fork below, and nowhere else.
The fork is a single point, and that is the whole of the argument. The statement heading each divergent block is itself common code, so both runs execute it at the same step of the same coupled sample — which gives the lemma’s first display, that \(\Pr [\Bad ]\) is the same number in the two executions rather than two numbers with one bound. Off \(\Bad \) there is no fork at all: the two runs are one run, so every fact of it has a single indicator there — the output, and, for game systems, \(\Win _{\op {Fin}}\) — and each difference of probabilities is at most the measure of the set where indicators may differ. That set is the lower branch, and its measure is \(\Pr [\Bad ]\).
Remark 11.3 (Nothing is assumed). The lemma asks nothing of the systems or of the slot: not well-formedness, not tightness, not refusal-obliviousness, and — worth savouring — not the absence of responsive calls. Every result that moves a machine pays a hypothesis for the move: Theorem 4.29 and Proposition 5.9 exclude responsive cores, Corollary 5.11 inherits the exclusion on both sides at once, and the notifying clock, the network and the channel sit outside all three for exactly that reason. The lemma above is indifferent — their responsive notifications hop as cheaply as anything else — because nothing is moved. Like the regrouping it is an identity about runs, resting on nothing but the determinism of an execution once its tapes are fixed, not a comparison of what two runs achieve. No budget appears for the same reason: exactness needs none, and Definition 4.30 enters only when an application sets about bounding \(\Pr [\Bad ]\).
Remark 11.4 (Why not by absorption). There is a tempting shorter route: absorb the whole execution into the environment — Lemma 4.18 exists to move machines — until each side is a single program, and quote [5] on the pair. It works where it works, and it is instructive to see why it is the worse lemma. Absorption’s hypotheses come along: the slot occupant moved must be refusal-oblivious, no core may place a responsive call on a ceded identity (Remark 9.4), and the environment’s \(\pars \) must hold no \(Z\)-identity — so the reduction proves the lemma only for the systems the dummy theorem already covers, and the notifying clock, for one, falls outside it. The direct coupling is no longer than the reduction and carries nothing: the machinery of Definition 4.17 was built for one execution rebracketed, and two executions coupled on equal tapes is the same induction with an easier case analysis — no relay, no rewriting of claims, no refusal to smooth over.
What the lemma is for, concretely. Emulation arguments hop between neighbouring ideal objects: a functionality and a lazier variant, a simulator and the same simulator with one check removed. Each hop is a pair identical until bad, the flags raised where the two part company, and the lemma prices the hop at \(\Pr [\Bad ]\) — in the same execution, against the same environment, with the occupants hopping alongside where a proof needs it. What remains is to bound \(\Pr [\Bad ]\), and that is generally a property: a finalization whose verdict is precisely that the raising condition occurred, priced by Definition 5.8 and inherited, where transfer applies, through Corollary 5.11. The canonical instance sits at the signature functionality of Chapter 15. Instrument \(\Fsig \) to raise \(\V {bad}\) where \(\op {Verify}\)’s honest-key test fires — an addition no caller can see, the flag being written and never read — and set beside it the variant that then lets the forgery stand. The two are identical until bad, and the hop between them costs the probability that a forgery is ever submitted — the quantity \(\op {FinUF}\) exists to police.