17.1 Functionality

\(\Fsig \) is local and randomized, and most of what was said about it concerned the simulator. The second example is its opposite on both counts. A clock functionality was introduced by Katz, Maurer, Tackmann and Zikas to model synchrony in UC [11]; recast by Badertscher, Maurer, Tschudi and Zikas as a shared setup around a monotone counter [3], it has become the canonical global functionality, the one the composable analyses of Bitcoin and its successors keep time by. The clock \(\Gclock \) below is that functionality in the language of this paper.

What it does is quickly said. The counter \(\V {now}\) starts at \(0\) and only ever steps forward. Anyone the clock serves may read it. Parties enter and leave the round structure through \(\op {Register}\) and \(\opl {Deregister}\), and the counter steps when every honest registered party has asked it to: \(\opl {Update}\) records a tick against the calling party, and once the honest registered ticks are all in, the test on line 17 advances the counter and clears them. A round ends exactly when the last honest party in it is done, and the adversary can neither stall the round nor close it early — how the code refuses each is below. Each recorded tick is reported to the adversary before \(\op {Update}\) returns, on line 20, responsively (Chapter 9) and with the answer discarded; what the notification buys and what it costs is settled at the end of Section 17.2. Every operation answers the counter as it stands on return, so the tick that closes a round learns the new time and the ticks before it the old; a party that must know where it stands reads again.

The fields.  The process id is a constant, \((\op {G}\op {Clock},0,0)\), where \(\Fsig \)’s was a parameter. Definition 1.2 then puts at most one copy in any system, which is the point: global means one instance, shared, and a second clock would be a second time. \(\admits := \Stdpid \cup \Apid \cup \Zpid \) makes \(\op {global}(\Gclock )\) hold by its first disjunct, so line 3 of \(\opl {Guard}\) waives the session check and every session reaches the one instance — the very separation the session component exists to make, deliberately not made here. A protocol that keeps time declares \((\Gclock ,\serves )\) in its \(\uses \), and the global disjunct of Definition 1.3 is what lets members of every session meet the entry at the shared copy. And \(\uses := \{(\Adv ,\serves )\}\) for the one call the code places, the notification of line 20. And \(\Ps \) stays a parameter but as the universe rather than the membership: it fixes the parties an interface exists for, while who is in the round structure at a given moment is state, entered and left through \(\op {Register}\) and \(\op {Deregister}\) as in [3] — dynamic membership is one more table, not a new kind of field.

Reading and ticking.  \(\admits \) is a field of the functionality, not of an operation, so one set governs every core, and the set above is the right one for \(\opl {Read}\): the adversary and the environment may ask the time — [3] lets both, and the environment reading the shared clock is much of what makes a global setup global. It is too wide for the three mutators, where an adversary free to act for a party could close a round the party had not finished, or drop it from the round structure altogether. The refinement sits as the first line of each core: a caller named \(A\) or \(Z\) acting for an honest party is answered the time and changes nothing, while at a corrupt party it passes — the adversary registers, deregisters and ticks for the parties it owns, as in [3], and those ticks are inert where it matters, line 17 never reading a corrupt party’s flag. One consequence deserves naming: while no honest party is registered the test of line 17 is vacuous, so the adversary may register a corrupt party and tick it freely — until the first honest registration, time is the adversary’s to spend, there too as in [3].

The quantifier of line 17 reads “every honest registered party”, and it is worth seeing how little of it \(\Gclock \) enforces itself. At a corrupt party a standard caller’s \(\op {Update}\) is handed to the adversary by line 4 of the full interface before the core runs, and the adversary’s own call at the same party is admitted by line 13; either way a corrupt party’s ticks are the adversary’s to give or withhold, and the \(\forall \) — which reads the register by the convention of Section 3.1 — ignores them regardless. Corrupt parties therefore neither hold a round open nor help close one. At an honest party both routes shut: \(\opl {Mediate}\) does not fire, and line 13 turns the observers’ ticks into reads. Monotonicity adds the last piece: a party corrupted after ticking leaves a stale flag behind, but it is outside the quantifier from then on, and the next advance clears it.

Three remarks on the code. Registrations and ticks are recorded against the party, not the caller: any machine acting for \(P\) may register or tick \(P\), \(\opl {Guard}\) having already tied the call to the party on line 2. [3] instead has every registered party and functionality tick separately before the round closes; that discipline, if wanted, is tables indexed by identity rather than party, and nothing else changes. The notification is \(\op {Update}\)’s alone; [3] tells the adversary about registrations and departures too, and extending line 20’s pattern to the other two mutators is mechanical. And \(\opl {Leak}\) returns the whole state, a clock keeping no secrets: the counter is anyone’s to read anyway, and the tables say only who is in the round and who is done with it.

Set against \(\Fsig \), most of what the signature example needed is still absent, each absence legible in the code. No value is the simulator’s to choose — the notification’s answer is discarded — so there is nothing to sanitize. And where \(\Fsig \) reached the slot through \(\Adv (\cdot )\) and re-tested its tables against what could happen while it hung, the clock’s one call is responsive by construction: every mutation of \(\op {Update}\) precedes line 20, and \(\opl {Respond}\) keeps the token from leaving, so no instance is ever re-entered mid-operation and there is nothing to re-test — enforced against every occupant of the slot, where Chapter 15 could only advise a simulator class. What the notification costs is recorded where it bites: Section 17.2 plays two properties over the clock and prices it there.