The channel of Chapter 19 was postulated. This chapter earns it: a protocol \(\rho \) over three ideal subroutines — a public-key directory, the unauthenticated network of Chapter 18, and the signatures of Chapter 15 — that UC-realizes an authenticated channel, and does so exactly, within \(0\), every subroutine being ideal and the whole reduction information-theoretic. It is the largest construction in the paper, and the one that exercises the most of it at once: composition, the responsive discipline, sanitization, tightness, and the fundamental lemma of Chapter 11 all appear, each doing a job no other could.
What \(\rho \) does. A party sending for the first time draws a signing key from \(\Fsig \) and registers it in the directory \(\Fpki \). To send \(\msg \) to \(Q\) it reads the clock for a timestamp \(\tau \), increments a per-party sequence number \(s\), signs the tuple \((\P ,Q,\tau ,s,\msg )\), and diffuses the tuple with its signature over \(\Fnet \). To fetch, it collects what \(\Fnet \) delivers, and keeps a diffused item only if it is addressed to the fetcher, carries a signature that verifies under the claimed sender’s directory key, and has a \((\text {sender},s)\) pair not seen before. What survives it hands up as \((\P ,Q,\tau ,\msg )\). Diffusion carries no addresses and no authenticity; the signature supplies the second and the address inside the signed tuple the first, so that a receiver trusts a sender’s name exactly because that name is under the sender’s own signature.
Why the target is \(\Facz \), not \(\Fac \). A corrupt sender is the obstruction, and it is instructive rather than incidental. Over a diffusion network the adversary writes on the wire whenever it likes, in particular during a fetch — \(\Fnet \)’s injections (line 16) are chosen inside the responsive window of the fetch that carries them. A message so injected, signed under a key the adversary registered for a corrupt party, is accepted by the receiver and delivered; but no prior \(\op {Send}\) ever placed it, so \(\Fac \), which delivers only what its own \(\op {Send}\) stored, cannot produce it, and no simulator can call \(\Fac .\op {Send}\) inside the fetch’s responsive window to repair the gap. Worse, the corrupt sender’s timestamp is its own to choose — the signature validates whatever \(\tau \) the payload carries — where \(\Fac \) stamps the true time of a call it witnessed. Neither gap is a defect in \(\rho \); both are what an authenticated diffusion unavoidably gives a corrupt party, and Chapter 20 closes with the argument that no protocol over these subroutines does better. So the realized object is \(\Facz \): \(\Fac \) with a corrupt sender’s traffic admitted at the fetch, unstored and freely timestamped, which is exactly the guarantee level of [7]’s authenticated channel and no less. The honest-sender guarantees — delivery by \(\Delta \), and authenticity, that an honest party’s fetched record was genuinely sent by the honest party it names — survive whole. And against an adversary that corrupts no one the two objects coincide: the fundamental lemma prices the difference at \(\Pr [\Bad ]\) for a \(\V {bad}\) that only a corrupt sender can raise, so \(\rho \) realizes \(\Fac \) itself, exactly, whenever nobody is corrupt (Corollary 20.2).
Two subroutines are not quite off the shelf. The signatures are the responsive variant \(\Fsig ^{!}\) of Chapter 9 — \(\Adv ^{!}\) in \(\opl {Gen}\), \(\opl {Sign}\) and \(\opl {Verify}\) — and the reason is the token. \(\Fac \)’s fetch is atomic: its one slot call is responsive, so no occupant drives the execution between the call and its answer. Were \(\rho \)’s fetch to reach \(\Fsig \) through the ordinary \(\Adv (\cdot )\), a verification would hand the adversary the token mid-fetch and let it act elsewhere before returning, an interleaving \(\Facz \)’s atomic fetch cannot show and no simulator could reproduce. The responsive variant \(\Fsig ^{!}\) removes the escape; \(\Fnet \)’s and \(\Facz \)’s calls are already responsive, so every send and every fetch is atomic on both sides. And the directory is local, not the global \(\Gpki \) of Chapter 16: a shared directory is written by an honest \(\rho .\op {Send}\) in the real world and read straight back by the environment through \(\opl {Retrieve}\), where in the ideal world nothing writes it and the simulator holds only the peek \(\Gpki \) grants at honest parties — an unsimulatable difference, the commitment problem of a global setup in this paper’s coordinates. A local \(\Fpki \), its identities private to the session like any hybrid, closes it; \(Z\) is kept out of its \(\admits \) for the same reason, a direct retrieval by the environment being a call the ideal world has no machine to serve.
The directory forgets bindings on purpose. \(\Fpki \) sanitizes a registered key to be a key and nothing more — per slot, dropping \(\Gpki \)’s cross-party freshness (Chapter 16, \(\Clean _{\op {reg}}\)). The freshness would be a weapon: the adversary chooses an honest party’s signing key, it being the value \(\Fsig .\op {Gen}\) returns, so it could pre-register that key at a corrupt slot and have the honest party’s own registration repaired to a different one, leaving directory and signing key disagreeing and the party’s every message rejected for ever — a denial of the liveness \(\Facz \) promises unconditionally. Per-slot fixity is enough because attribution never rested on binding: the sender’s name travels inside the signed tuple, the receiver looks that name up, and a signature valid under an honest party’s key on a tuple naming a different sender is a forgery \(\Fsig \) suppresses. Binding buys nothing here and costs liveness, so it goes.
Local directory \(\Fpki \)
\(\PID \), \(\Ps \), \(\admits \), \(\uses := \emptyset \), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\op {Register}(\vk )\) from \(\id '\)
auto
\(\id .\op {Retrieve}(P)\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
\(\Clean _{\op {key}}(\vk )\):
\(\Facz \) is \(\Fac \) with one operation changed: \(\op {Fetch}\) takes back a pair \((S,I)\) from the slot, \(S\) the early releases among stored ids as before, \(I\) a set of injected records the slot delivers unstored. Sanitizing pins each injection to a corrupt sender and to the fetching party, so an injection can only ever put a corrupt party’s word into the fetch that asked for it; \(\Fac \)’s own \(\op {Send}\), \(\op {Leak}\) and \(\op {Initialize}\) are unchanged.
Functionality \(\Facz \): the fetch of \(\Fac \), replaced
fields as \(\Fac \) (Section 19.1)
\(\id .\op {Fetch}()\) from \(\id '\)
\(\Clean _{\op {inj}}(I;\ \Cs , P_f)\):
The protocol reads its four subroutines through the interfaces at the party being served, the notation \(\id _{\F } := (\F .\PID ,\id .P)\) of Chapter 18. Its \(\uses \) names all four, the clock among them, since \(\rho \) stamps its own payloads and does not recover \(\Fnet \)’s stamp, which \(\Fnet \) never returns.
Protocol \(\rho \) over \(\{\Fpki ,\Fnet ,\Fsig ^{!}\}\)
\(\PID \), \(\Ps \), \(\admits \), \(\uses := \{(\Fpki ,\serves ),\allowbreak (\Fnet ,\serves ),\allowbreak (\Fsig ^{!},\serves ),\allowbreak (\Gclock ,\serves )\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\op {Send}(Q,\msg )\) from \(\id '\)
auto
\(\id .\op {Fetch}()\) from \(\id '\)
The simulator. Fix an occupant \(\Adv \) of the adversary slot. In the real world \(\Adv \) faces the three hybrids; in the ideal world they are gone, and \(\Sim _{\Adv }\) must present their faces from inside itself. It is an absorption (Definition 4.26, read on the adversary side): \(\Sim _{\Adv }\) bundles \(\Adv \) with one internal copy each of \(\Fpki \), \(\Fnet \) and \(\Fsig ^{!}\), runs \(\Adv \) against them exactly as the real execution would, and drives them from what \(\Facz \) tells it. On an honest \(\op {Send}\) notification \(\Facz \) hands it \((\P ,Q,\tau ,\msg )\); it advances the internal \(\V {seq}\) for \(\P \), forms \(x = (\P ,Q,\tau ,s,\msg )\), and replays \(\rho \)’s own steps into the internal hybrids — an internal \(\Fsig ^{!}.\op {Sign}\), whose \(\Adv ^{!}\) query the hosted \(\Adv \) answers, and an internal \(\Fnet .\op {Send}\), whose notification it delivers — so the hosted \(\Adv \) sees precisely the queries the real world would place. When \(\Facz \) makes its responsive fetch query, \(\Sim _{\Adv }\) runs \(\rho .\op {Fetch}\)’s filter over the internal \(\Fnet \)’s delivery against the hosted \(\Adv \), learns exactly which records \(\rho \) would hand up, and answers \((S,I)\): the ripe or early-released honest entries by their \(\Facz \) ids in \(S\), and the corrupt-sender records — those verifying under a key registered at a corrupt slot — in \(I\). Corruption it passes straight through, \(\op {Corrupt}\) surviving the bundle as Remark 3.2’s does.
Made explicit: two pieces of state the paragraph above passes over silently, both forced by the code just above it rather than chosen. \(\Facz \)’s own \(\op {Send}\) (inherited from \(\Fac \), Section 19.1) notifies the slot with \((\op {Send},m,Q,\tau ,\msg )\), \(m\) its own list index — not \((\P ,Q,\tau ,\msg )\) alone, the sender \(\P \) read off the identity the query arrives at (Definition 9.2). The simulator \(\Sim _{\Adv }\) must keep that index, \(\V {fid}\) below, to name the entry later; it cannot recover it at fetch time, having no access to \(\Facz .\V {list}\) itself. And \(\rho \)’s own tables — \(\V {gen}\) at line 5, \(\V {seq}\), and the \(\V {seen}\) its freshness test reads at line 24 — are tables \(\Sim _{\Adv }\) does not host, \(\rho \) being no part of the ideal world and only its subroutines internal here, so reproducing its filter needs shadows of its own, kept equal to \(\rho \)’s by construction rather than by reading them.
Two routing questions the prose leaves open, and both decide whether the simulator works at all. The first is what becomes of a call the hosted \(\Adv \) places on \(\rho \)’s own identity. Line 3 admits \(\Adv \) at a corrupt party and neither mediation hook fires on its calls, so in the real world such a call reaches \(\rho \)’s core — and every subroutine call that core then places is mediated straight back to \(\Adv \) (line 4, the caller being \(\rho \) and the party corrupt), so nothing of it ever reaches \(\Fnet \)’s buffer. Relayed outward it would instead reach \(\Facz \), whose \(\op {Send}\) files a record that ripens and is delivered by \(\Delta \) whatever the slot answers (Section 19.1) — a delivery with no real-world counterpart. So these calls are not relayed: Definition 4.13’s explicit routing keeps them inside, where the last handler below runs \(\rho \)’s core against the hosted \(\Adv \) exactly as \(\opl {Mediate}\) does really. The outward set is declared accordingly.
The second is how far a responsive answer reaches. Both handlers answer a responsive call, and \(\opl {Respond}\) (Definition 9.1) refuses every call the responder places; calls between two hosted machines are not placed at all (Definition 4.13), so the internal copies are reachable, but nothing outside the bundle is. Two things outside it would otherwise be reached, and \(\Sim _{\Adv }\)’s code avoids each.
A hosted copy’s full interface opens by reading the corruption register, which Definition 9.2 refuses outright — a responsive answer is computed from what the responder already knows. So the handlers drive the copies through their cores, written \(\opl {Gen}\) rather than \(\fopl {Gen}\) above, and nothing is lost by it: a party corrupt at the send or the fetch is mediated before \(\Facz \)’s own core runs, so no slot query is ever issued on its behalf and no handler ever serves one, and at an honest party the full interface adds only its silencer — the gate passes, and neither hook fires. And \(\Fnet \) opens both \(\op {Send}\) and \(\op {Fetch}\) by reading \(\Gclock \), which is shared rather than hosted. That read is answered with the \(\tau \) the notification or query already carries, which is the right value and not merely a convenient one: on the send it is the stamp the proof shows \(\rho \)’s and \(\Fnet \)’s own reads share, and on the fetch it is \(\Facz \)’s read, which no responsive call can have advanced past (Proposition 9.3).
Simulator \(\Sim _{\Adv }\)
occupies \(\IDs (\Adv )\); hosts \(\Adv \) and one internal copy each of \(\Fpki \), \(\Fnet \), \(\Fsig ^{!}\) (Definition 4.26, read on the adversary side); outward
set the identities the ideal execution still serves, less \(\rho \)’s own, which the last handler routes by hand
(Definition 4.13)
\(\op {Initialize}()\):
on \(\Facz \)’s \(\op {Send}\) note \((m,Q,\tau ,\msg )\) at \(\P \)
auto
on \(\Facz \)’s responsive \(\op {Fetch}\) query \((\tau )\) at \(Q\)
on \(\Adv \)’s \(\op {Send}\) or \(\op {Fetch}\) at a corrupt \(\P \)
Routing, and \(\op {Corrupt}\)
Three things about \(\Sim _{\Adv }\)’s code, all used by the proof but easy to read past. First, \(\V {fid}[\P ,s] \neq \unset \) at line 26 is exactly “an undrained \(\V {list}\) entry matches the record” in the proof’s own words: \(\Sim _{\Adv }\) recognizes a record precisely when it once relayed the honest \(\op {Send}\) that produced it, which is the only way an entry gets into \(\V {fid}\) at all.
Second, \(\V {gen}\) is a shadow of \(\rho \)’s own flag and not a reading of the internal \(\Fpki \)’s \(\V {VK}\), though at an honest party the two agree — \(\Fpki \)’s \(\op {Register}\) turns an \(A\)- or \(Z\)-caller’s call there into a peek at its line 4, so only \(\rho \) ever writes that entry. They part company at a corrupt one, which is why the shortcut is not taken: there \(\rho \)’s \(\op {Register}\) is mediated away before \(\Fpki \)’s core runs, leaving \(\V {VK}[\P ]\) unset while \(\rho \) sets \(\V {gen}[\P ] \gets 1\) regardless, \(\rho .\op {Send}\)’s line 5 not reading the answer. A simulator testing \(\V {VK}\) would re-run \(\op {Gen}\) and \(\op {Register}\) on the party’s every later send and show the hosted \(\Adv \) a pair of queries the real \(\Adv \) never sees.
Third, line 26 puts every matching honest record into \(S\), ripe ones included, where \(\Facz \) would have taken the ripe ones through \(R\) on its own. This is deliberate and costs nothing: \(\Clean _{\op {addr}}\) admits any undrained entry addressed to \(Q\), and \(\Facz .\op {Fetch}\) unions \(R\) with \(S\) at its line 7 and drains their union, so naming a ripe entry twice delivers and drains it once. Naming it is also all \(\Sim _{\Adv }\) can do, having no clock read of its own inside the query with which to tell ripe from early.
Theorem 20.1 (\(\rho \) realizes the authenticated channel). Let \(\pi := \{\rho ,\Fpki ,\Fnet ,\Fsig ^{!}\}\) with parameters matched so that \(\pi \cup \{\Gclock \}\) is well-formed, \(\rho .\admits = \Facz .\admits \), and \(\Fnet .\pars = \Facz .\pars = \Delta \). Then \(\pi \) UC-emulates \(\{\Facz \}\) within \(0\): for every occupant \(\Adv \) of the adversary slot the simulator \(\Sim _{\Adv }\) above gives, for every \(\Zenv \in \ZenvSet _{\pi ,\{\Facz \}}\),
equal as distributions. The quantifier is over every adversary, not the dummy alone: every slot call in either world is responsive, so Theorem 4.29 does not reach this and the simulator is exhibited against each \(\Adv \) directly.
Proof. One induction on activations, carrying an invariant in three parts. The coupling pairs machine to machine as in Lemma 4.18, so the routing, claims and refusal arguments are that lemma’s; what is new is the state carried across the \(\rho \)/\(\Facz \) cut, and the invariant on it is the whole of the argument. The invariant states the three parts: the internal hybrids hold what the real ones hold, \(\Sim _{\Adv }\)’s shadows hold what \(\rho \) holds, and \(\Facz .\V {list}\) holds exactly the undrained honest sends. Three cases preserve it. Send shows the two worlds stamp a send at the same time, and that replaying \(\rho \)’s own steps into the internal copies keeps them equal. Fetch carries the weight: it splits not on the sender’s current status but on whether an undrained \(\V {list}\) entry matches the record, and shows that the unmatched case forces a corrupt sender — which is what unforgeability buys here, and why \(\Clean _{\op {inj}}\) never trips. Corrupt-party traffic covers the one activation the declared outward set withholds, and shows that withholding it is what the invariant needs. Couple the two executions on equal tapes, paired machine to paired machine as in Lemma 4.18: \(\Zenv \), \(\Corr \) and \(\Gclock \) each to itself, the hosted \(\Adv \) and the internal hybrids of \(\Sim _{\Adv }\) to the real \(\Adv \) and the real hybrids, and \(\rho \) together with what the hybrids hold to \(\Facz \). Everything below is one induction on activations, in the shape of Definition 4.17; the claims and refusal paragraphs are Lemma 4.18’s verbatim, and its routing paragraph holds of every call but one — \(\Sim _{\Adv }\) is a bundle, and the calls that cross its boundary are the ordinary outward and inward relays, save those the hosted \(\Adv \) places on \(\rho \)’s own identities, which the declared outward set withholds and the last handler serves inside — so only the state carried across the \(\rho \)/\(\Facz \) cut is new, and the invariant on it is the whole of the argument.
The invariant. At every corresponding pair of configurations: (i) the internal \(\Fpki \), \(\Fnet \) and \(\Fsig ^{!}\) of \(\Sim _{\Adv }\) hold the same tables as the real hybrids, having been initialised alike and driven by the same calls in the same order; (ii) \(\Sim _{\Adv }\)’s shadow \(\V {gen}\), \(\V {seq}\) and \(\V {seen}\) equal \(\rho \)’s; and (iii) \(\Facz .\V {list}\) holds exactly the records \((P,Q,\tau ,\msg )\) of the sends \(\rho \) made through a party’s own \(\op {Send}\) while that party was honest — one entry per such \(\rho .\op {Send}\), at the timestamp it read — that no fetch has since drained, and no others. Later corruption of the sender does not disturb the entry, corruption being monotone and the record already placed. (i) and (ii) hold because paired copies run the same code on equal tapes under the same driving: at an honest party \(\rho \)’s core drives the real hybrids and \(\Sim _{\Adv }\)’s handlers drive their copies through the same steps, and at a corrupt one both sides mediate the same subroutine calls away before any callee’s core runs, as the third case below checks. (iii) is what the three cases preserve.
Send. \(\Zenv \) calls \(\op {Send}(Q,\msg )\) at an honest \(\P \). On the ideal side \(\Facz .\op {Send}\) reads the clock, appends \((\P ,Q,\tau ,\msg )\) to \(\V {list}\), and notifies \(\Sim _{\Adv }\) responsively. On the real side \(\rho .\op {Send}\) reads the clock, and its internal \(\Fnet .\op {Send}\) reads it again; the two clock reads coincide, by the argument of Section 18.2 — no core of either execution runs between them, \(\Gclock .\op {Read}\) placing no call — so the send is stamped \(\tau \) on both sides. \(\Sim _{\Adv }\), notified, replays exactly the \(\op {Gen}\)/\(\op {Register}\)/\(\op {Sign}\)/\(\op {Send}\) steps \(\rho \) runs, into copies that (i) keeps equal to \(\rho \)’s — the internal \(\Fnet \)’s own clock read answered with the \(\tau \) the notification carried, which is that same stamp, since the responder may place no call of its own to make it — and the hosted \(\Adv \) answers each \(\Adv ^{!}\) query as the real \(\Adv \) does over equal tapes. Both return \(\ok \); one new \(\V {list}\) entry matches the one send; (iii) holds.
Fetch. \(\Zenv \) calls \(\op {Fetch}()\) at \(Q\). Everything turns on the two worlds delivering the same set \(M\), and on \(\Sim _{\Adv }\) being able to name it within \(\Clean _{\op {inj}}\). Run \(\rho .\op {Fetch}\)’s filter, which \(\Sim _{\Adv }\) mirrors internally: a delivered record \((P,Q,\tau ,\msg )\) is one whose diffused tuple \((x,\sigma )\), \(x = (P,Q,\tau ,s,\msg )\), is addressed to \(Q\), carries a signature verifying under \(\V {VK}_{\Fpki }[P]\), and is fresh in \(\V {seen}[Q]\). Split not on \(P\)’s current status but on whether an undrained \(\V {list}\) entry matches the record — the honest case and the injected case being exactly these two.
If one matches: by (iii) it is a send \(\rho \) made for \(P\) while \(P\) was honest, and \(\Facz \) delivers it from store — through \(R\) if ripe, and through \(S\), its id admitted by \(\Clean _{\op {addr}}\) as addressed to \(Q\), if \(\Sim _{\Adv }\) releases it early to match \(\Fnet \)’s early release. Whether or not the sender is corrupt by now, the record is delivered from \(\V {list}\) and never injected, so none is delivered twice.
If none matches: then \(P\) is corrupt at the fetch, and this is where unforgeability earns its place. Were \(P\) honest at the fetch it would be honest throughout, by monotonicity, so \(\V {VK}_{\Fpki }[P]\) would be \(P\)’s own \(\Fsig \) key — \(\rho \) registers exactly what \(\op {Gen}\) returned — and a signature verifying under an honest party’s key is never a forgery: \(\op {Verify}\)’s honest-key test (Section 15.1) sets \(b \gets 0\) on any fresh triple under such a key, so \(b = 1\) forces the triple recorded, and only an honest \(\op {Sign}\) records one, which by (iii) would leave a matching \(\V {list}\) entry — against the case. So \(P \in \Cs \); the record is the adversary’s to have produced, an \(\Fnet \) injection or a signature made as a corrupt party, and \(\Sim _{\Adv }\) places \((P,Q,\tau ,\msg )\) in \(I\), which \(\Clean _{\op {inj}}\) admits, \(P\) being corrupt and \(Q\) the fetcher. The channel \(\Facz \) delivers it unstored, as \(\rho \) hands it up. This is what unforgeability buys: no record lacking a genuine send behind it can ever wear an honest name, so the injection channel is only ever asked for corrupt senders, and \(\Clean _{\op {inj}}\) never trips.
Freshness matches on both sides by (ii), and draining matches: a stored record delivered is drained from \(\V {list}\) ideally and marked seen really, so \(\Fnet \)’s re-delivery of the same tuple is filtered by \(\V {seen}\) really and finds no \(\V {list}\) entry ideally, falling into neither case a second time. So the two \(\op {Fetch}\)es return the same \(M\) and step to corresponding configurations; (iii) is preserved, its stored entries drained in lockstep.
Corrupt-party traffic. \(\Adv \) calls \(\op {Send}\) or \(\op {Fetch}\) at a corrupt \(\P \), on \(\rho \)’s own identity — the one activation the outward set withholds, and the case the two above do not reach. The full interface admits it at line 3, \(\P \) being corrupt, and neither hook fires on an \(A\)-caller, so on the real side \(\rho \)’s core runs. Every subroutine call that core then places carries \(\rho \)’s name at a corrupt party, so line 4 of that same interface hands each to \(\Adv \) before the callee’s core runs: nothing of the activation reaches \(\Fnet \)’s buffer, \(\Fpki \)’s directory or \(\Fsig \)’s tables, and its very timestamp is \(\Adv \)’s to supply. \(\Sim _{\Adv }\)’s line 30 runs that same core against the hosted \(\Adv \) on the same shadows, so both sides move \(\V {gen}\), \(\V {seq}\) and \(\V {seen}\) alike and leave the hybrids untouched, preserving (i) and (ii); and neither side touches \(\V {list}\) — ideally because the call never leaves \(\Sim _{\Adv }\), really because there is no \(\Facz \) to touch — so (iii) is preserved with nothing to check.
Withholding these calls is what (iii) needs, and it is worth saying why rather than leaving it to the routing. Relayed outward the call would reach \(\Facz .\op {Send}\), which files a record at the true time; the ripeness test \(\Facz \) inherits at \(\Fac .\op {Fetch}\)’s line 12 would then deliver it to \(Q\) within \(\Delta \) whatever the slot answered, where the real world delivers nothing at all unless \(\Adv \) injects on its own account. The entry would break (iii) the moment it was filed, and no later answer of \(\Sim _{\Adv }\)’s could retract it — \(R\) being \(\Facz \)’s to compute. This is the ripening that Section 19.1 charges to a corrupt sender speaking through \(\Fac .\op {Send}\), and a protocol whose corrupt parties speak through \(\Fnet \) instead does not pay it.
No other activation touches the cut: a call among \(\Zenv \), \(\Gclock \), \(\Corr \) and \(\Adv \) that targets none of \(\rho \)’s identities is routed and claimed identically on both sides by Lemma 4.18, and reads no state the invariant governs. Corresponding halting configurations return \(\Zenv \)’s one output. The executions are equal as distributions, and the advantage is \(0\) — not a bound but an identity, every step deterministic once the tapes are fixed and no forgery ever slipping through to force an injection the sanitizer would refuse. □
The bound is \(0\), and it is worth being clear on why nothing weaker was available and nothing stronger was needed. Every subroutine is ideal, so there is no computational gap to charge for; the reduction is an identity of distributions, as the composition theorem’s is. Transfer, note, does not run here: Corollary 5.11 wants cores placing no responsive call, and \(\rho \)’s reach \(\Fsig ^{!}\), \(\Fnet \) and the clock all responsively, so a property of \(\Facz \) does not descend to \(\pi \) for free — it must be re-proved over \(\pi \), exactly as Section 17.2 warned for anything built over the notifying clock. What the theorem gives instead is the stronger thing for a realization: not a bound against the dummy but an equality against every adversary.
Corollary 20.2 (Against non-corrupting classes, \(\rho \) realizes \(\Fac \) itself). Instrument \(\Facz \) to set \(\V {bad} \gets \true \) at line 7 when \(I \neq \emptyset \), and let \(\Fac ^{\flat }\) be the pair-shaped \(\Fac \) that ignores \(I\) — its fetch \(\Fac \)’s, taking \((S,I)\) and using \(S\) alone. Now \(\Facz \) and \(\Fac ^{\flat }\) are identical until bad (Definition 11.1), the injection the one bad-guarded difference. So for occupants and environments that corrupt nobody, \(\Clean _{\op {inj}}\) forces \(I = \emptyset \) and \(\Pr [\Bad ] = 0\), whence by Lemma 11.2 the two are indistinguishable and \(\pi \) UC-emulates \(\{\Fac ^{\flat }\}\), hence \(\{\Fac \}\), within \(0\) against the non-corrupting classes. Corrupt a party and the guarantee is \(\Facz \)’s, no less: the honest-sender half of \(\op {FinAuth}\) (Section 19.2) transfers, its \(\op {Send}\)-tracing argument reading only honest records, while the full \(\op {FinAuth}\) fails of \(\Facz \) exactly as it does of \(\Fnet \), and for the same reason.
Remark 20.3 (The weakening is forced). No protocol over \(\{\Fpki ,\Fnet ,\Fsig ^{!}\}\) realizes \(\Fac \) as shipped, so \(\Facz \) is not a convenience but the true target. Suppose one did. A corrupt party diffuses, inside a fetch’s responsive window, a well-formed item its receiver accepts — \(\Fnet \) grants exactly this, the wire being the adversary’s to write (Section 18.1) — carrying a timestamp \(\tau ^{*}\) of the adversary’s choosing. On the ideal side the accepting fetch is atomic, so the simulator must have called \(\Fac .\op {Send}\) strictly earlier to place a matching entry; but \(\Fac \) stamps that call the true time it was made, not \(\tau ^{*}\), and the receiver reads \(\tau ^{*}\) off the delivered record. An environment that sends at one time and has its corrupt confederate claim another distinguishes with certainty. The freedom is \(\Fnet \)’s to give and no receiver-side check removes it, since the signature validates whatever time the payload carries; only weakening the ideal object to admit it — which is \(\Facz \) — closes the gap. This is the diffusion analogue of the impossibility that forces \(\Fnet \)’s own injections to sit outside its delivery guarantee.
This is the paper’s longest single construction, and the point of running it in full is that every layer of the framework shows up load-bearing. Composition supplies the cut between \(\rho \) and its hybrids; the responsive discipline of Chapter 9 makes both fetches atomic so the schedules can be coupled at all; sanitization confines a corrupt slot to corrupt senders; tightness would be what a property of \(\Facz \) needs to descend, and its absence under responsive cores is why the realization is proved directly rather than inherited; and the fundamental lemma of Chapter 11 is what turns the exact realization of the weaker object into the exact realization of the stronger one wherever no corruption is in play. The authenticated channel, postulated in Chapter 19, is now a theorem.