19.1 Functionality

\(\Fnet \) diffuses and nobody signs. The complementary object is the one where every message arrives with its sender attached and none arrives from nobody — the authenticated channel of [7], given the same \(\Delta \) and the same clock. The channel \(\Fac \) below is that functionality, and the two are worth reading side by side: they differ in a good deal more than the sender field, and the difference is where authentication actually lives.

What it does is quickly said. The operation \(\op {Send}\) takes a recipient as well as a message, stamps the pair by the clock, files it under a fresh index, and tells the adversary — authentication is not secrecy, and this channel hides nothing at all. The operation \(\op {Fetch}\) gathers everything addressed to the fetching party that has come of age, asks the adversary which of the rest to release early, answers the union, and empties the entries it answered. What the receiver gets is the whole record: sender, recipient, send time, message. The division of power is \(\Fnet \)’s — the adversary chooses when within \(\Delta \) and in what order — and so is the bound: an entry \(\Delta \) old is in the next fetch of the party it names, whatever the slot answers.

The fields.  They are \(\Fnet \)’s, for \(\Fnet \)’s reasons. \(\PID \), \(\Ps \) and \(\admits \) are parameters, one instance per session, with \(\admits \) naming the protocol served in the local pattern of Chapter 1, and \(\pars := \Delta \). The \(\uses \) field is \(\{(\Gclock ,\serves ),(\Adv ,\serves )\}\), its clock entry met at the shared copy by the global disjunct of Definition 1.3. Both conjuncts of \(\serves \) are needed and neither is a formality: the first asks the clock to serve every party the channel does, and without the second the channel’s own name would not be admitted at the clock, so \(\opl {Guard}\) would refuse every read on line 4.

Authentication is the adversary’s own interface.  \(\Fnet \) needs line 16 because a diffusion channel gives adversarial traffic no name to enter under: the wire is anonymous, so forgery is modelled by letting the slot write on it directly. Here there is a name, and the full interface already delivers it. At a corrupt sender the adversary reaches the core — lines 3 and 4 admit \(\Adv \) at a corrupt party and neither mediation hook fires on its calls, both testing \(\id '.F \neq A\) — so corrupt traffic enters through \(\op {Send}\) under the sender’s own identity, timestamped by the clock like anyone’s. The channel \(\Fac \) therefore has no injections and needs none, and the sender field of an entry is not a report about the wire but a fact about which interface the call came through. That is what an authenticated channel is: forgery is impossible because there is nowhere to forge from.

The price is that adversarial traffic ripens. A message the adversary sends from a corrupt party is in the list with a real timestamp, so line 12 will deliver it by \(\Delta \) and no later answer can retract it. The network \(\Fnet \) refuses this deliberately, filing injections at \(\infty \) so the guarantee is for the honest and never conscripts the slot’s own traffic. The difference is a consequence of addressing rather than a choice made against it: a message with a named sender and a named recipient is a message the sender is on the record for, and holding the adversary to the deadline it accepted when it spoke as a corrupt party is the reading that keeps the sender field meaning what it says.

Fetching empties.  Each entry names one recipient, so answering it discharges it, and line 16 clears what line 12 and the slot between them selected. The network \(\Fnet \) cannot do this — a diffused message is owed to everyone — which is why it carries the sticky \(\V {rel}\) table instead and re-answers what it has already answered. The two guarantees are different in kind and neither implies the other: \(\Fnet \)’s is that a party’s view only grows, \(\Fac \)’s that a message is delivered exactly once. A protocol over \(\Fnet \) must deduplicate and one over \(\Fac \) must not lose what it fetched, and each obligation is the other’s absence.

Sanitizing the release.  The slot’s answer is a set of indices to release early, and the only thing wrong it can be is a set naming entries that are not the fetching party’s — or not entries at all. Chapter 12’s procedure repairs exactly this kind of fault, so line 14 runs the answer through it under

with the list and the fetching party as the read-only context. Two things follow that are worth saying, because they are what makes \(\San \) the right instrument here rather than an assertion. A good value always exists, so the footnote of Chapter 12 has nothing to prove in this case: \(\emptyset \) satisfies \(\Clean _{\op {addr}}\) whatever the list holds, and being the empty set it is also the lexicographically first such, so a failing answer is repaired to no early release at all. And that repair costs the adversary nothing it could not have had, since an adversary wanting some particular good subset released may submit that subset and be returned it untouched. An assertion in \(\San \)’s place would read the same on good answers and hand the slot a denial of service on bad ones — one stray index and the honest party’s fetch dies — which is the failure Chapter 12 exists to rule out.

Both slot calls are responsive.  The clock’s discipline, and here it is load-bearing in a way worth spelling out. The operation \(\op {Fetch}\) reads the time on line 10 and asks the slot on line 13. Were that call not responsive the adversary would hold the token in between and could drive the clock forward before answering; \(\tau \) would then be stale by the time line 12 used it, fewer entries would clear \(\tau _i + \Delta \leq \tau \), and a message past its deadline would be lawfully withheld. Responsiveness is what makes the read and the test one moment. The operation \(\op {Send}\) mutates before it notifies and needs no such argument, but is responsive too, for \(\Fnet \)’s reason: nothing else may run inside either call.

Three remarks on the code. The recipient is not checked against \(\Ps \) on \(\op {Send}\): a message addressed outside the channel’s parties is filed and never fetched, which is the same silence a party who declines to fetch would produce, and the guarantee below is a statement about entries someone fetches. The send time travels with the message, so a receiver can date what it receives and check the deadline itself — \(\Fnet \)’s fetch returns no such thing, and the difference is that \(\Fac \)’s \(\Delta \) is locally auditable where \(\Fnet \)’s is only a fact about the functionality. And \(\opl {Leak}\) returns the list entire, the channel keeping no secrets: its contents were told to the adversary at line 7 as they arrived, and what has since been drained is what the slot itself watched leave.