F-Net — Δ-delayed diffusion network

F-Net (Δ-delayed diffusion network) is part of Channels, Agreement, Ledgers in the UC functionality encyclopedia. Status: a canonical, well-established UC functionality.

A clock-parameterized specialization of unauthenticated diffusion (see F-diffuse): messages are timestamped against the global clock and guaranteed to reach every party within a fixed delay \(\Delta\), following Katz–Maurer–Tackmann–Zikas’s bounded-delay model and Badertscher–Maurer–Tschudi–Zikas’s diffusion form — the network the composable analyses of Bitcoin and its successors run over. It is unauthenticated: a fetched message carries no sender, and the adversary may inject fresh traffic with no name attached at all. The companion functionality with sender identity attached is F-AC.

Functionality

Reading the box: \(\mathcal{A}^{!}(\cdot)\) is a responsive call on the adversary slot, so a fetch reads one consistent snapshot rather than racing the clock; \(\mathit{id}_{\mathcal{G}_{\mathsf{Clock}}}.\mathsf{FullRead}()\) is a call on the global clock’s full interface, guard included; \(\mathcal{M}\) is the message space; \(\Delta\), the parameter on the header line, is the delivery deadline every entry is measured against.

Functionality \(\mathcal{F}_{\mathsf{Net}}\)
\(\mathit{pid}\),   \(\mathbf{P}\),   \(\mathbf{N}\),   \(\mathbf{U} := \{(\mathcal{G}_{\mathsf{Clock}},\mathsf{serves}),\,(\mathcal{A},\mathsf{serves})\}\),   \(\mathit{par} := \Delta\)
Initialize():
  1. \(\mathtt{ctr} \gets 0\)
  2. \(\mathtt{buf} \gets \varnothing\)// entries \((m, P, \mathit{msg}, \tau)\)
  3. \(\mathtt{rel} : \mathbb{N} \times \mathcal{F}_{\mathsf{Net}}.\mathbf{P} \to \{0,1\}\)
  4. \(\mathtt{rel}[*,*] \gets 0\)// what is released to whom
id.Send(msg)from id′
  1. \(\tau \gets \mathit{id}_{\mathcal{G}_{\mathsf{Clock}}}.\mathsf{FullRead}() \text{ as } \mathit{id}\)
  2. \(m \gets \mathtt{ctr}\);  \(\mathtt{ctr} \gets \mathtt{ctr} + 1\)
  3. \(\mathtt{buf} \gets \mathtt{buf} \cup \{(m, \mathit{id}.P, \mathit{msg}, \tau)\}\)
  4. \(\mathcal{A}^{!}\bigl(\mathit{id}.\mathsf{Send},\ m,\ \mathit{msg}\bigr)\)// the network is public
  5. \(\textbf{return}\ m\)
id.Leak()from id′
  1. \(\textbf{return}\ (\mathtt{buf},\ \mathtt{rel})\)
id.Fetch()from id′
  1. \(\tau \gets \mathit{id}_{\mathcal{G}_{\mathsf{Clock}}}.\mathsf{FullRead}() \text{ as } \mathit{id}\)
  2. \((S, I) \gets \mathcal{A}^{!}\bigl(\mathit{id}.\mathsf{Fetch},\ \tau\bigr)\)// a non-pair reads as \((\varnothing,\varnothing)\)
  3. \(S \gets S \cap \{m : (m,\cdot,\cdot,\cdot) \in \mathtt{buf}\}\);
  4. \(I \gets I \cap \mathcal{M}\)// sanitized inline
  5. \(\mathtt{rel}[m, \mathit{id}.P] \gets 1\)  for each \(m \in S\)
  6. for each \(\mathit{msg} \in I\):
  7. \(\mathtt{buf} \gets \mathtt{buf} \cup \{(\mathtt{ctr}, \bot, \mathit{msg}, \infty)\}\);
  8. \(\mathtt{rel}[\mathtt{ctr}, \mathit{id}.P] \gets 1\);  \(\mathtt{ctr} \gets \mathtt{ctr} + 1\)
  9. \(\textbf{return}\ \bigl\{(m, \mathit{msg}) : (m, P', \mathit{msg}, \tau_s) \in \mathtt{buf}\)
  10. \({}\wedge\ \bigl(\mathtt{rel}[m, \mathit{id}.P] = 1 \ \vee\ \tau_s + \Delta \leq \tau\bigr)\bigr\}\)

The box is transcribed from UC for Gamers (§18.1, p. 169), line numbering and all. There is no addressee anywhere in the state: an entry is \((m, P, \mathit{msg}, \tau)\), and delivery is diffusion to everyone the instance serves. What \(\mathtt{rel}\) tracks is not whether a message reaches a party but when — it is early release, not routing.

Send stamps the entry with the clock’s current time (line 5) and tells the adversary about it (line 8) before returning, because the network is public: there is nothing to hide about a message in flight, only about when it lands.

The two lines to read closely are in Fetch:

  • Line 20 reads \(\mathtt{rel}\) or the deadline. The adversary may release an entry to a party early, but \(\tau_s + \Delta \leq \tau\) delivers it regardless once the deadline passes — so silence past \(\Delta\) is ignored rather than punished, and this disjunction is the whole of liveness.
  • Lines 13–14 sanitize the slot’s answer inline rather than through \(\mathsf{San}[\mathsf{Clean}]\): \(S\) is intersected down to ids actually in the buffer and \(I\) down to genuine messages, so a malformed or greedy answer is trimmed rather than refused. A non-pair reads as \((\emptyset, \emptyset)\), which is why no answer at all is a safe answer.

Injected messages (lines 16–18) are filed with \(\bot\) where a sender would go and \(\infty\) where a send time would, then marked released to the fetching party alone. They therefore carry no sender, never ripen for anyone else, and reach exactly the party the adversary handed them to — the adversary’s own traffic, on the wire only because it wrote there. That the send notification and the fetch query are both responsive is what keeps a fetch’s clock read and its aging test one atomic moment.

Known realizations

Not itself realized by a lower-level protocol in this framework; it stands in directly for whatever best-effort broadcast/gossip network a deployment actually has. What is built on top of it: the authenticated channel is realized by signing every message with a signature functionality key registered in a directory, then diffusing signature and message together over F-Net — see F-AC’s own entry.

Properties

Both proven with probability exactly \(0\) against every occupant of the adversary slot:

  • Liveness. A message sent by an honest party at time \(\tau_s\) is present in every fetch an honest party makes from time \(\tau_s + \Delta\) on, regardless of what the adversary answered along the way.
  • Authentication does not hold, and provably so: there is a concrete environment and adversary strategy — inject a message with no prior send at all — that wins the “every fetched message was actually sent” game with probability exactly \(1\). This is not a bug but the definition of unauthenticated diffusion: the wire has no names on it, so nothing stops the adversary writing on it directly. This is the fact that motivates F-AC, the addressed, authenticated variant that closes exactly this gap.

Formal artifacts

No machine-checked formalization yet.

References: