Section 18.1 left three properties unformulated: delivery by \(\Delta \), monotone views, and no delivery before sending. The last needs no game at all: an id not yet in \(\V {buf}\) is nothing \(S\) can name, line 20 intersecting with \(\V {buf}\) before anything else runs, so no occupant of the slot can ever release what has not yet been sent. Monotone views we still leave unformulated, being a property of \(\V {rel}\) alone and orthogonal to timing. What we formalize here is the first, under the name \(\opl {FinLive}\), liveness: a message ripened by \(\Delta \) is missing from no later honest fetch. And we formalize a property \(\Fnet \) was never claimed to have, \(\opl {FinAuth}\), authentication: a message an honest party fetches was sent by someone. Both take the search reading of Definition 5.8.
They are two finalizations of one game, and this is where that shape earns the most. The network \(\Fnet \) has the first outright and, being an unauthenticated diffusion by design — Section 18.1’s own remark on the injections of line 16 — provably lacks the second: one shell, one set of oracles, one trace, and two verdicts read off it of which one is unwinnable and the other is won with probability \(1\). Under two separate games that would be two statements about two objects; here it is one object measured twice. What keeps the measurements apart is Remark 5.3’s single flag: an environment that calls \(\op {FinAuth}\) has closed the game against \(\op {FinLive}\), so no run is judged on both, and nothing about the pair is a conjunction.
Both are played over the game system \(\gamma := \{\Gm \} \cup \{\Fnet ,\Gclock \}\), with \(\Fnet .\admits := \{\Gm .\PID \}\) pinned and \(\Fnet .\Ps \subseteq \Gm .\Ps \) — Section 15.2’s tightness argument transplanted whole, since \(\Fnet \)’s own fields already follow \(\Fsig \)’s pattern rather than the clock’s (Section 18.1). The interface box below states \(\Gm .\uses \) in full. No caller but \(\Gm \) passes \(\opl {Guard}\) at \(\Fnet \): not the environment, not the adversary, not a machine hosted at an invented instance of the game’s name. So every message \(\Fnet \)’s core ever stores, and every answer it ever returns to a \(\op {Fetch}\), passes through the relays below and is recorded — a game whose verdict names “sent by someone” has no other way to know it. \(\Fnet \)’s own dependence on the clock and the slot is unaffected by any of this and is met exactly as it was for \(\Fnet \) itself, the clock at the shared copy by the global disjunct of Definition 1.3. Inside an interface at \(\id \) we write \(\id _{\Fnet }\) for \((\Fnet .\PID ,\id .P)\) and \(\id _{\Gclock }\) for \((\Gclock .\PID ,\id .P)\), the second the notation of Section 17.2.
Game shell over \(\Fnet \) and \(\Gclock \); the finalizations follow
\(\PID := (\Gm .F,0,0)\), \(\Ps := \Fnet .\Ps \cup \{Z\}\), \(\admits := \Zpid \), \(\uses := \{(\Fnet ,\serves _{\Gm }),\,(\Gclock ,\serves )\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\opdef {Send}(\msg )\) from \(\id '\)
auto
\(\id .\opdef {Fetch}()\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
The finalizations of \(\Gm \); the shell over \(\Fnet \) and \(\Gclock \) is shared
\(\id .\opdef {FinLive}()\) from \(\id '\) (liveness)
\(\id .\opdef {FinAuth}()\) from \(\id '\) (authentication)
Three things about the code. Neither relay reads \(\op {Send}\)’s or \(\op {Fetch}\)’s own return value for a timestamp — there is none to read — so both read the clock themselves, one line above the call to \(\Fnet \); the two readings coincide because no core of \(\gamma \) runs between them, not \(\Fnet \)’s own guard and corruption check, which only reads \(\Cs \) and finds \(\id .P\) honest, the relay having run at all, and not \(\op {Read}\) itself, which places no call (Section 17.1). Neither relay excludes \(\id .P = Z\), unlike Section 17.2’s: \(\Fnet \)’s fields follow \(\Fsig \)’s pattern and not the clock’s, and neither verdict reads any the worse for the root sending or fetching too — so the shell is spared the demand steadiness made of the clock’s, and both finalizations get the shell they would have asked for alone. And authentication’s verdict asks nothing of a sender, because \(\op {Fetch}\) returns none to ask about — the fetched pair is \((m,\msg )\) alone, and whether some \(m\) was ever sent, by whom, is exactly the fact no caller of \(\Fnet \) can otherwise recover, which is what the whole game is testing.
Proposition 18.1 (\(\Fnet \) has liveness). For every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {FinLive}}] = 0\). So \(\{\Fnet ,\Gclock \}\) has liveness within \(0\) against \(\bigl (\ZenvSet _{\gamma ,\gamma },\Xset \bigr )\) in the sense of Definition 5.8, for \(\Xset \) the class of all occupants.
Proof. Suppose \((\atom {send},P,m,\tau _s,\msg ) \in \V {tr}\), written at some activation of the \(\op {Send}\) relay. Its own clock read and \(\Fnet .\op {Send}\)’s internal one (Section 18.1) answer the same value, by the argument just given, so the core stores exactly \((m,P,\msg ,\tau _s)\) in \(\V {buf}\).
Now suppose also \((\atom {fetch},Q,\tau ,M) \in \V {tr}\) with \(\tau \geq \tau _s + \Delta \). \(\Fnet .\op {Fetch}\)’s core returns every pair \((m',\msg ')\) with \((m',P',\msg ',\tau _{s'}) \in \V {buf}\) and \(\V {rel}[m',Q] = 1 \vee \tau _{s'} + \Delta \leq \tau \) (line 20), \(\tau \) its own reading of the clock and, again, the relay’s. Taking \(m' = m\): the buffer entry is \((m,P,\msg ,\tau _s)\) and \(\tau _s + \Delta \leq \tau \) holds by hypothesis, so the second disjunct is met whatever \(\V {rel}[m,Q]\) is and whatever the slot answered at line 12, which settles only \(S\) and \(I\) and neither disjunct. Hence \((m,\msg ) \in M\), and line 18 gives \(0\). □
Proposition 18.2 (\(\Fnet \) does not have authentication). There are \(\Zenv ^{*} \in \ZenvSet _{\gamma ,\gamma }\) and an occupant \(\mathcal {X}^{*}\) of the adversary slot with \(\Pr [\Win _{\op {FinAuth}}] = 1\): no \(\varepsilon < 1\) bounds \(\{\Fnet ,\Gclock \}\)’s authentication against any class containing them.
Proof. A counterexample in two machines. The occupant \(\mathcal {X}^{*}\) answers \(\Fnet \)’s fetch query with one injection and places no call — which is exactly why it is not the dummy, whose only way to answer is to relay to the environment, a call \(\opl {Respond}\) refuses. That difference is the whole point of stating these properties over every occupant of the slot rather than the dummy alone: read at the dummy, \(\op {FinAuth}\) would come out satisfied, and only vacuously. The environment \(\Zenv ^{*}\) then fetches once and finalizes on \(\op {FinAuth}\) and nothing else. The injection survives sanitizing, reaches the trace, and no \(\op {Send}\) relay ever ran, so the verdict fires with advantage \(1\). Let \(\mathcal {X}^{*}\) have \(\Adv \)’s fields but place no call. On the query \(\id .\op {A}(\id ''.\op {Fetch},\tau )\) with \(\id ''.F = \Fnet .\PID \) — the shape of line 12 — it returns \((\emptyset ,\{\msg ^{*}\})\) for one fixed \(\msg ^{*} \in \Msgs \); on anything else it returns \(\none \). Placing no call, it is never refused by \(\opl {Respond}\) at either of \(\Fnet \)’s slot calls, unlike the dummy, whose only way to answer is to relay to \(\Zenv \) (line 5), a call \(\opl {Respond}\) does refuse (Remark 9.4). This is exactly where \(\mathcal {X}^{*}\) differs from \(\Dum \), and exactly why Propositions 15.1, 17.2 and 18.1 are stated over every occupant of the slot and not the dummy alone — the dummy’s case of Definition 5.8, with \(\mathcal {X}\) dropped from the subscript, would read \(\op {FinAuth}\) as satisfied, and only vacuously, \(\Dum \) being unable to inject at all.
Let \(\Zenv ^{*}\) claim \((\Gm .\PID ,Q)\) for \(Q \in \Fnet .\Ps \), call \(\op {Fetch}()\) once, then claim \((\Gm .\PID ,Z)\) and call \(\op {FinAuth}()\) — and \(\op {FinAuth}\) and no other, which is the whole of what it takes to be judged on this property and not the one beside it. It corrupts no one, hosts nothing, and claims only identities of \(\Gm \)’s own name, so \(\Zenv ^{*} \in \ZenvSet _{\gamma ,\gamma }\).
At that fetch, \(I = \{\msg ^{*}\}\) survives sanitizing (\(I \gets I \cap \Msgs \)), so the loop of line 16 adds some fresh \((m,\none ,\msg ^{*},\infty )\) to \(\V {buf}\) and sets \(\V {rel}[m,Q] \gets 1\); \((m,\msg ^{*})\) is returned, and \((\atom {fetch},Q,\tau ,M) \in \V {tr}\) with \((m,\msg ^{*}) \in M\). No \(\op {Send}\) relay ever ran, so \(\V {tr}\) carries no entry \((\atom {send},\cdot ,m,\cdot ,\msg ^{*})\) — indeed no \(\atom {send}\) entry naming \(m\) at all, \(m\) being fresh to the injection. So \(Q \notin \Cs \) throughout, and line 27 gives \(1\).
Nothing about that run touches Proposition 18.1. The environment \(\Zenv ^{*}\) closed the game at \(\op {FinAuth}\), so \(\op {FinLive}\) was never answered and \(\Win _{\op {FinLive}}\) did not occur: the two events are disjoint by Remark 5.3, and the same shell can therefore host a property it always keeps beside one it always loses without the two saying anything about each other. □
As with \(\Gclock \), liveness transfers by Corollary 5.11 only if the cores of the game system place no responsive call, and both of \(\Fnet \)’s do, lines 8 and 12; a system \(\pi \) put in place of \(\{\Fnet ,\Gclock \}\) must then have the transfer argued directly, for the reason Remark 9.4 gives, exactly as the clock’s own notification cost Section 17.2 the same thing. Tightness, note, did no work in either proof above beyond licensing \(\gamma \) as a game system: unlike correctness and unforgeability, neither verdict here needs to rule out a message entering \(\V {buf}\) by some route \(\Gm \) never sees, only to read off what happens to what \(\Gm \) itself placed — so both propositions would survive a weaker dependence, were one wanted, though nothing above asks for it.
Authentication transfers nothing, having nothing to transfer: Proposition 18.2 is not a bound to inherit but a fact about the specification, exactly the fact Section 18.1 already asserted in prose — proved now rather than merely said, and by an adversary no stranger than one that ignores its mail. No replacement of \(\{\Fnet ,\Gclock \}\) is asked to improve on it. What does have the analogous property is Chapter 19’s \(\Fac \): a corrupt sender’s traffic there enters through \(\op {Send}\) itself, under its own identity, rather than through an unaccountable slot answer (Chapter 19, “Authentication is the adversary’s own interface”), so the fetched pair carries a sender for a verdict to name, and there the transplanted win condition — fetched, addressed, and never sent — is not met.