\(\Gclock \) carried two properties for having two kinds of promise — a local one, that the counter moves as coded, and a global one, that it moves only when everyone honest has agreed. The directory \(\Gpki \) splits the same way, and into two finalizations of one game. \(\opl {FinFix}\), fixity, says a registered key never changes — the local promise, about one party’s own entry. \(\opl {FinBind}\), binding, says no two parties ever hold the same key — the global one, quantified over all of \(\Gpki .\Ps \) at once. Both take the search reading of Definition 5.8.
Both are played over the game system \(\gamma := \{\Gm \} \cup \{\Gpki \}\), with \(\Gpki \) taken as in Section 16.1 save one field: \(\admits := \{\Gm .\PID \}\), pinned — Remark 6.5’s forcing, exactly as for the clock (Section 17.2), and for the identical reason: a property of a global \(\F \) is a property against an adversary that shares it, and fixity and binding are both claims about every key there is, certifiable only where the game’s trace is all there is.
Pinned, the directory is no longer global, so line 3 asks for one session and the experiment’s own session \(0\) meets it. No caller but \(\Gm \) passes line 2: not the environment, not a machine it hosts, and not the adversary’s \(A\)-identities, refused before line 4 could even apply. So every key \(\Gpki \) ever holds enters through the relay below and is recorded — a game whose verdict is “two parties share a key” has no other way to know it. Inside an interface at \(\id \) we write \(\id _{\Gpki }\) for \((\Gpki .\PID ,\id .P)\).
Game shell over \(\Gpki \); the finalizations follow
\(\PID := (\Gm .F,0,0)\), \(\Ps := \Gpki .\Ps \cup \{Z\}\), \(\admits := \Zpid \), \(\uses := \{(\Gpki ,\serves _{\Gm })\}\), \(\pars := \none \)
\(\op {Initialize}()\):
\(\id .\opdef {Register}(\vk )\) from \(\id '\)
\(\id .\op {Leak}()\) from \(\id '\)
auto
\(\id .\opdef {Retrieve}(P)\) from \(\id '\)
The finalizations of \(\Gm \); the shell over \(\Gpki \) is shared
\(\id .\opdef {FinFix}()\) from \(\id '\) (fixity)
\(\id .\opdef {FinBind}()\) from \(\id '\) (binding)
Two things about the code. The operation \(\op {Retrieve}\) is relayed and logged though neither verdict reads its trace: a game that could not look anyone’s key up would not be exercising \(\Gpki \) at all, and leaving the interface whole costs nothing, exactly as \(\Gclock \)’s shell relayed \(\op {Read}\) for games that read only the mutators. And \(\op {FinFix}\)’s verdict does not need \(\vk _1\) and \(\vk _2\) ordered, unlike steadiness’s reading of its trace: idempotence means at most one of the two calls that produced them can be the write, the other only a later read of it, and either order loses the game identically, a changed key being a changed key whichever one came first.
Proposition 16.1 (\(\Gpki \) has fixity). For every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {FinFix}}] = 0\). So \(\{\Gpki \}\) has fixity 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 {reg},P,\vk _1),(\atom {reg},P,\vk _2) \in \V {tr}\) with \(P \notin \Cs \). By tightness both were logged at line 5, each running \(\Gpki .\op {Register}\)’s own core at \(\id .P = P\): the relay’s own name is \(\Gm \)’s, not \(A\) or \(Z\), so line 4 never intercepts it. The core’s only write is line 8, reached only while \(\V {VK}[P] = \unset \), and once reached it fixes \(\V {VK}[P]\) to some sanitized value for good — every later call at \(P\) finds \(\V {VK}[P] \neq \unset \) and returns line 6’s value, the same one, unchanged. So the two calls producing \(\vk _1\) and \(\vk _2\) agree: whichever ran first wrote the value, and the other only read it back. The verdict at line 17 gives \(0\). □
Proposition 16.2 (\(\Gpki \) has binding). For every \(\Zenv \in \ZenvSet _{\gamma ,\gamma }\) and every occupant \(\mathcal {X}\) of the adversary slot, \(\Pr [\Win _{\op {FinBind}}] = 0\). So \(\{\Gpki \}\) has binding 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 {reg},P,\vk ),(\atom {reg},Q,\vk ) \in \V {tr}\) with \(P,Q \notin \Cs \) and \(P \neq Q\). By Proposition 16.1’s argument \(\vk = \V {VK}[P]\) and \(\vk = \V {VK}[Q]\) from the moment each was first written onward. Say \(Q\)’s write came second, the case \(P\)’s symmetric; at that moment \(\op {Register}\)’s line 8 ran \(\vk \gets \San [\Clean _{\op {reg}}](\cdot ;\V {VK})\) with \(\V {VK}[P]\) already set, and \(\San \)’s guarantee (Chapter 12) is that its output satisfies \(\Clean _{\op {reg}}\) whatever the input — membership in \(\Keys \) and freshness against every key already on file, \(P\)’s among them. So \(Q\)’s write cannot equal \(\V {VK}[P]\), contradicting \(\vk = \V {VK}[P] = \V {VK}[Q]\). The verdict at line 25 gives \(0\). □
Both transfer by Corollary 5.11 with nothing extra to argue. The hypothesis it asks — that the game system’s cores place no responsive call — is met the cheap way: \(\Gpki \)’s cores place no call of any kind, responsive or not, so Remark 9.4’s caveat never arises and dummy completeness (Section 4.4) is untouched. Unlike \(\Gclock \), whose notification bought locality at inheritance’s expense, and unlike \(\Fnet \) and \(\Fac \), whose slot calls priced their own transfer, \(\Gpki \) pays nothing: a system \(\pi \) put in place of \(\{\Gpki \}\) inherits fixity and binding directly, the four conditions of Section 15.2’s closing paragraph being the only ones left to discharge. A directory that asks the adversary nothing has nothing to spend.