F-AC — Δ-delayed authenticated channel

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

Canetti’s authenticated channel, given the same clock-relative \(\Delta\) delivery bound as F-Net. Where F-Net diffuses anonymously and lets the adversary inject unattributed traffic, F-AC names a sender and recipient on every message and admits no injections at all — every delivered message really was sent, by the party it names, because the only way onto the channel is through its own Send interface. 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 (on the wire for F-Net, nowhere but the interface for F-AC).

Functionality

Reading the box: \(\mathcal{A}^{!}(\cdot)\) is a responsive call on the adversary slot; \(\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. One predicate is named but not written out — \(\mathsf{Clean}_{\mathsf{addr}}(S; \mathtt{list}, P)\), defined in the source’s prose, holds exactly when \(S \subseteq \{i : \mathtt{list}[i] = (\cdot, P, \cdot, \cdot)\}\).

Functionality \(\mathcal{F}_{\mathsf{AC}}\)
\(\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{list} : \mathbb{N} \to (\mathcal{F}_{\mathsf{AC}}.\mathbf{P}^{2} \times \mathbb{N} \times \mathcal{M}) \cup \{\bot\}\)
  3. \(\mathtt{list}[*] \gets \bot\)// entries \((P, Q, \tau, \mathit{msg})\)
id.Send(Q, msg)from id′
  1. \(\tau \gets \mathit{id}_{\mathcal{G}_{\mathsf{Clock}}}.\mathsf{FullRead}() \text{ as } \mathit{id}\)
  2. \(\mathtt{ctr} \gets \mathtt{ctr} + 1\)
  3. \(\mathtt{list}[\mathtt{ctr}] \gets (\mathit{id}.P,\, Q,\, \tau,\, \mathit{msg})\)
  4. \(\mathcal{A}^{!}\bigl(\mathit{id}.\mathsf{Send},\ \mathtt{ctr},\ Q,\ \tau,\ \mathit{msg}\bigr)\)
  5. \(\textbf{return}\) ok
id.Leak()from id′
  1. \(\textbf{return}\ \mathtt{list}\)
id.Fetch()from id′
  1. \(\tau \gets \mathit{id}_{\mathcal{G}_{\mathsf{Clock}}}.\mathsf{FullRead}() \text{ as } \mathit{id}\)
  2. \(R \gets \{m : \mathtt{list}[m] = (\cdot,\, \mathit{id}.P,\, \tau_m,\, \cdot)\)
  3. \({}\wedge\ \tau_m + \Delta \leq \tau\}\)// come of age
  4. \(S \gets \mathcal{A}^{!}\bigl(\mathit{id}.\mathsf{Fetch},\ \tau\bigr)\)// released early
  5. \(S \gets \mathsf{San}[\mathsf{Clean}_{\mathsf{addr}}]\bigl(S;\ \mathtt{list},\, \mathit{id}.P\bigr)\)
  6. \(M \gets \{\mathtt{list}[m] : m \in R \cup S\}\)
  7. \(\mathtt{list}[m] \gets \bot\)  for each \(m \in R \cup S\)
  8. \(\textbf{return}\ M\)

The box is transcribed from UC for Gamers (§19.1, p. 178), line numbering and all. Every entry carries both a sender and a recipient, which is the structural difference from F-Net and the source of everything else.

Send files the entry under the caller’s own identity, \(\mathit{id}.P\) (line 6), and that is the whole authentication mechanism: a corrupt sender’s call goes through this same interface under its own name, and there is no other way onto the channel, so nothing is ever attributed to a party that did not call Send. Note what Send returns — \(\mathsf{ok}\), not the message id — so a sender cannot refer to its own message afterwards; the channel gives it no handle to withdraw or re-address.

Fetch answers in two halves and then destroys what it answered:

  • Lines 11–12 gather what has come of age on the clock alone: entries addressed to the fetching party, sent at least \(\Delta\) ago. This half needs no adversary at all, which is why liveness holds no matter what the slot says.
  • Lines 13–14 let the adversary release entries early, and \(\mathsf{Clean}_{\mathsf{addr}}\) bounds what that permission is worth: only undrained entries already addressed to the fetching party, with a bad answer repaired to \(\emptyset\). The adversary can hurry a message along; it cannot redirect one or conjure one.
  • Line 16 drains every entry the call is about to return, so each message is delivered exactly once rather than re-offered on every fetch the way F-Net’s diffused entries are.

Both slot calls are responsive, for the same reason as F-Net’s: a fetch’s clock read and its aging test have to be one atomic moment, or the adversary could stall between them and withhold a message past its deadline. Leak returns the whole list, since authentication is not secrecy and this channel hides nothing.

Known realizations

Realized exactly, within advantage \(0\), by a protocol over three purely local, ideal subroutines: a public-key directory, F-Net, and a (responsive) signature functionality. To send, a party registers a signing key on first use, then signs the tuple (sender, recipient, timestamp, sequence number, message) and diffuses it with its signature over F-Net; to fetch, it keeps only diffused items addressed to itself whose signature verifies under the claimed sender’s directory key and whose (sender, sequence number) pair hasn’t been seen before. The reduction is information-theoretic — every subroutine is already ideal, so there is no computational gap to account for.

One genuine subtlety: this construction realizes a very slightly weaker object, \(F\text{-}AC^\flat\), that admits a corrupt sender’s traffic at fetch time unstored and with a freely-chosen timestamp — exactly Canetti’s own authenticated-channel guarantee level, no less, no more. The gap is forced: a diffusion network lets the adversary inject traffic mid-fetch with no prior send, so no simulator can make F-AC itself (which delivers only what its own Send stored) produce a corrupt sender’s message on demand. Against an adversary that corrupts nobody, the two objects coincide exactly, so the construction realizes F-AC itself whenever no party is corrupted.

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\), to an honest or corrupt recipient, is present in every fetch the recipient makes from time \(\tau_s + \Delta\) on.
  • Authentication. Every message an honest party fetches really was sent, by exactly the party it names — there is no environment/adversary pair that can make an honest recipient accept a message with no matching prior send, unlike F-Net, where the symmetric claim is false by an explicit counterexample.

Formal artifacts

No machine-checked formalization yet.

References:

  • Canetti. Universally composable security. Journal of the ACM, 67(5):28:1–28:94, 2020.
  • Badertscher, Maurer, Tschudi, and Zikas. Bitcoin as a transaction ledger: A composable treatment. In Advances in Cryptology – CRYPTO 2017, Part I, volume 10401 of LNCS, pages 324–356, 2017.
  • UC for Gamers, this site’s own book draft on composable security. Chapters “Δ-Delayed Authenticated Channel” and “Realizing the Authenticated Channel” give the functionality, its properties, and the full realization proof.