Chapter 5
Properties

Emulation compares two systems. A property asks something of one: that no adversary win a game played against it — which Proposition 5.9 will reduce to the dummy’s not winning, the slot absorbing into the environment. Little new machinery is wanted for either. A game is a functionality like any other, the environment is the adversary that plays it, and the plumbing of the previous sections already settles who may call what — so a property is a system, an environment class, and an event, and the fields of Definition 1.1 do most of the work that a game’s rules do on paper. What has to be added is small, and is named as it comes: one hygiene condition on the game system, and the three conditions Section 4.4 already asks of anything it moves.

One game, then, may carry several properties: \(\op {FinCor}\) and \(\op {FinUF}\) over a signature functionality, say, sharing the oracles that record what was signed and differing only in the verdict read off them at the close. The environment chooses which to be judged on by choosing which finalization to call, and that choice is the last thing it does. So a game with several finalizations is not a conjunction of properties but a shell holding several, each with its own advantage below; an environment that maximizes one need not maximize another, and nothing here asks it to.

Each field is forced, and it is worth saying by what.

The process id.  There is one game per experiment, so the session and instance carry no information and we fix both at \(0\). Session \(0\) is not a convention but a requirement: the environment reaches \(\Gm \) by claiming its own \(Z\)-identity, which line 2 admits because \(\Zpid \subseteq \Gm .\admits \), and line 3 then asks \(\Gm .s = \Zenv .s = 0\) — \(\Gm \) not being global. Remark 7.17 is that observation in general. By Definition 1.3 a local \(\F \) shares the caller’s session, so the whole experiment sits in session \(0\), which is where the machines the execution supplies live too.

The served parties.  A core claims only its own identity (line 5) and \(\opl {Guard}\) asks \(\id '.P = \id .P\), so \(\Gm \) at party \(P\) reaches \(\F \) at party \(P\) and at no other: the game exercises \(\F \) one party at a time, and the environment chooses the party by choosing which identity of \(\Gm \) to address, its root being free to act for any by line 3. Hence \(\F .\Ps \). The root is added for the finalizations, and the next paragraph says why.

The admitted callers.  \(\Zpid \) and nothing else. Not \(\Stdpid \), which would make \(\Gm \) global and let any standard functionality finalize the game; not \(\Apid \), which would hand it to the adversary. With \(\Zpid \) alone, line 2 refuses every caller but the environment.

The name.  Arbitrary, and Corollary 7.16 says so: renaming the game and \(\F .\admits \) together changes no probability, so a property proved against a game of one name holds against it under every other. This matters because line 5 lets the game claim only its own identity, so \(\F .\admits \) has to name the game while the \(\F \) that ships inside a protocol names that protocol; the corollary is what makes the two the same property. What is not arbitrary is the caller’s code, which no renaming touches.

The dependence.  \(\serves _{\Gm }\) exempts the root because the root is the game’s own bookkeeping identity: \(\F \) need not serve a party the game never calls it at. A game whose verdict must query \(\F \) — verifying a claimed forgery, say — has two options, and they are the usual ones: record during the oracle calls whatever the verdict needs, or ask \(\F \) to serve the root as well, when \(\serves _{\Gm }\) becomes \(\serves \).

Tightness.  The fields above do not suffice on their own, and the gap is Remark 6.5’s. An admissible environment is silenced on \(\ncl {\gamma }\), so it may claim no identity of a name \(\gamma \) uses — but Definition 4.10 forbids it only from hosting at identities \(\gamma \) occupies, and a hosted functionality is a full interface claiming its own identity through its own silencer (Definition 4.13). So an environment may host a machine at an unoccupied process id of a used name: at \((\Gm .F,0,1)\), say, an invented second instance of the game’s own name. A member of \(\sigma \) that admits its caller by name — the local pattern of Chapter 1 — admits that machine, and its calls pass every line of \(\opl {Guard}\): the name lies in \(\admits \), the parties agree, the sessions agree, and \(\opl {Mediate}\) does not fire at an honest party. The environment would then hold an oracle on \(\F \) that the game records nothing of, and \(\Pr [\Win _{\op {Fin}}] = 1\) for any game whose verdict is that the adversary produced something it was not given.

Tightness at \(\{\Gm \}\) refuses that, and refuses it completely. Every member but the game admits whole process ids the system occupies, so an invented instance fails line 2; and Remark 6.5’s party condition makes every identity a pinned caller could speak from occupied, where Definition 4.10 forbids hosting. The one route tightness leaves open — to a member of \(I\) itself, which here is the game — is closed by \(\Gm .\admits = \Zpid \): a hosted functionality is standard and claims a standard process id, which \(\Zpid \) excludes, while the environment’s own \(Z\)-identities are not hosted but its own. The game is thus the one member that may admit a bare class of process ids, and it is safe in doing so exactly because \(Z\) is no standard name.

Which environments may play is settled by the class Chapter 4 already defines, taken at a single system.

The two clauses say what a game needs them to say. Silenced on the name closure, an environment may claim no identity of a name \(\gamma \) uses, so it cannot speak as \(\F \), as one of \(\F \)’s subroutines, or as a further instance of any of them; what it may claim is its own \(Z\)-identities, which reach \(\Gm \), and fresh names, which reach only what admits all of \(\Stdpid \). So the environment plays the game through \(\Gm \)’s interfaces and touches \(\F \) directly only when \(\F \) is global — and then it touches it as anyone may, which is what being global means and what Definition 4.10 already grants in the emulation setting. A property of a global \(\F \) is therefore a property against an adversary that shares it, and the game must be written knowing that. The hosting clause is the occupancy hygiene of Definition 3.3, and it also stops the environment from installing a second game.

Since one flag closes the game (Remark 5.3), at most one \(\Win _{\op {Fin}}\) occurs in any run: the events of distinct finalizations are disjoint, and a game with several of them is several properties measured in several executions rather than several numbers read off one.

Under the decision reading the advantage is signed, where that of Definition 4.5 is not, and the asymmetry is the point: an environment cannot flip \(\Win _{\op {Fin}}\) as it can flip a guess, the event being the game’s verdict rather than its own, so a game it cannot win scores \(-1\) and there is nothing to take an absolute value of.

\(\Win _{\op {Fin}}\) is an event of the execution rather than its output, and that is deliberate: an execution’s output is whatever the environment returns (Chapter 4), and a property is not a guess to be reported but a thing that happened. Nothing is lost by the distinction, because Remark 5.2 makes the two agree where it matters. The bit line 10 computes is the bit the finalization hands the environment, unmediated, so we may name the environment that reports it: for a fixed \(\op {Fin}\), write \(\Zenv ^{\star }\) for \(\Zenv \) with its return at the root replaced by “return \(1\) if any call I placed on \((\Gm .\PID ,Z).\fopl {Fin}\) was answered with \(1\), and \(0\) otherwise”. Every part of that earns its place. The identity is named because a finalization addressed at another party fails line 8 where that party is honest and is answered by the adversary where it is corrupt, so the value coming back need not be the game’s; at the root neither happens, by Remark 5.2. The operation is named because \(Z \in \Gm .\Ps \), so line 1 serves every interface of \(\Gm \) at the root, the game’s own oracles included — and because with several finalizations the reporting form must say which property it is reporting on, one \(\Zenv ^{\star }\) per \(\op {Fin}\). The test is against \(1\) rather than a reading of the answer as a bit, because a later finalization comes back \(\rej \) by Remark 5.3, and \(\rej \) is no bit (Section 3.6). And it is any call rather than the first, because the first one placed may be refused — an environment claiming \((Z,P)\) for \(P \neq Z\) fails line 2’s party test, leaving \(\done \) unset — while a later one is served; nothing is weakened by quantifying, since at most one call is ever answered with \(1\), the game serving one finalization and refusing the rest. So \(\opl {Exec}\) returns \(1\) exactly when \(\Win _{\op {Fin}}\) occurs, and \(\Zenv ^{\star }\) can compute it, every call on that interface being one it placed itself: \(\Gm .\admits = \Zpid \) admits no other caller, and a functionality the environment hosts claims a standard id, which \(\Zpid \) excludes. Then

the two machines placing the same calls and differing only in the value they halt with. That also puts \(\Zenv ^{\star }\) in every class \(\Zenv \) is in whose membership turns on \(\pars \) and hosting alone — \(\ZenvSet _{\gamma ,\gamma }\) among them, and the budgeted classes of Definition 4.30 up to the one further step of reading a bit back. Proposition 5.10 is where all of this is used.

Why the dummy.  The default slot occupant is the dummy of Section 4.4, and the reason is that a game has one adversary and it is the environment. The dummy relays in both directions and keeps no strategy, so an environment driving it holds everything the slot can do; and where \(\F \)’s own cores reach the adversary — the \(\Adv (\cdot )\) of Section 3.4, which is how an ideal functionality leaves a value unpinned — it is then the environment that answers, which is exactly the freedom a game means to give it. Dropping \(\mathcal {X}\) from the subscript for the dummy’s case is thus no loss of generality but a choice of who plays; the longer form is kept because Proposition 5.10 needs a simulator in that slot. That the abbreviation costs nothing is not a matter of taste, and the reason is the construction of Section 4.4: the slot absorbs into the environment.

The hypotheses are Theorem 4.29’s and no more: a game system placing responsive calls is outside this, by Remark 9.4, and so is an environment that silences its own \(Z\)-identities, the instruction of Definition 4.26 leaving under a \(Z\)-claim. Neither is a condition on what the occupant does, which is the point — a game need not care whether the machine in the slot plays fairly, only that it can be moved.

One scope condition comes with all of this, and it is the same one throughout. The proposition above rests on the regrouping of Theorem 4.29, which holds only for systems whose cores place no responsive calls, Remark 9.4 showing where the relay fails otherwise; the same condition governs Theorem 4.29 itself, which is what supplies the emulation hypothesis Proposition 5.10 wants from a wider adversary class, and Corollary 5.11 inherits it on both sides at once. A game system whose \(\F \) reaches the slot through \(\Adv ^{!}\) therefore sits outside all three and must have its dummy-only hypothesis established directly. What a responsive theory of games would look like we leave where Remark 9.4 leaves it.

The calibration.  Which of Definition 5.8’s two readings a finalization takes is not a matter of taste, and the rule is this. The factor \(2\Pr [\Win _{\op {Fin}}] - 1\) reads the property as a decision: an environment that guesses wins with probability \(\tfrac 12\) and scores \(0\), and one that always wins scores \(1\). That is right where guessing is a strategy — where the verdict is a bit the environment could have flipped a coin for. It is wrong for a search property — unforgeability, say, where winning is meant to be hard outright — because there the same quantity reads \(\Pr [\Win _{\op {Fin}}] = (1 + \padv {\op {Fin}}{\Gm ,\sigma ,\Zenv })/2\), so a bound \(\varepsilon \) on the advantage is a bound \((1+\varepsilon )/2\) on the winning probability, which for small \(\varepsilon \) is the wrong scale: an \(\varepsilon \) of \(0\) would permit a forger succeeding half the time. Search properties therefore take \(\Pr [\Win _{\op {Fin}}]\) itself. Declaring the reading per finalization rather than fixing one globally is what lets a single shell carry both kinds at once. Every property in this paper is of the second kind — winning each of the games below is meant to be impossible outright, not merely no better than a guess — so all of them take the search reading; the decision reading is there for properties where guessing is the strategy, an indistinguishability written as a game among them.

The choice is not free, and Proposition 5.10 is where it is paid for. Its two displays are the same bound at the two scales — \(2\varepsilon \) for the decision reading, \(\varepsilon \) for the search reading — so each finalization inherits transfer at the scale its own reading fixes, and a game mixing the two inherits at both.

Finally, the reason to define properties this way rather than beside the framework: emulation carries them.

Two things about that proof. The reduction is the textbook one, and absorption is what makes it so: the absorbed environment \(\Zenv ^{\star \,\gamma \setminus \varphi }\) of Definition 4.15 hosts the game itself along with the rest of \(\gamma \setminus \varphi \), so “an environment playing the game against \(\pi \)” becomes “an environment distinguishing \(\pi \) from \(\varphi \)” by moving the game inside it, which is what Theorem 4.20 was proved about. And the property on the right is stated against \(\Sim \) in the slot rather than against the dummy, which is why Definition 5.8 keeps the occupant as an argument — but it is not an obligation anyone need meet in that form, because the slot absorbs into the environment as well.

The reduction is worth drawing, because it is one move and the move is easy to read past. It is the commuting square of Figure 1 again, in the same conventions and with the dotted box again marking the pair being exchanged — but this time it is the game that moves:

Read it by watching \(\Gm \). In the left column it sits inside the system, where a game belongs: the environment plays it, and \(\Win _{\op {Fin}}\) is the verdict it returns. In the right column it sits inside the dashed box, part of the machine doing the distinguishing. Crossing that boundary is the whole reduction — an environment playing the game against \(\pi \) becomes an environment telling \(\pi \) from \(\varphi \) — and once the game is across, what is left is a bare emulation question, which is what Theorem 4.20 was proved about.

The two horizontal edges are free. The reporting form only rewrites what \(\Zenv \) returns at the root, leaving every call it places untouched, so it changes no run; and absorption is Lemma 4.18, an identity of executions rather than a bound. So the right edge is the only thing paid for, and it is the hypothesis applied at \(\Dum \) — which is why the bottom row carries \(\Sim \) in the slot and not the dummy, and so why Definition 5.8 keeps the occupant as an argument at all. The left edge is then forced, exactly as in Figure 1: chasing the square makes the two \(\approx _\varepsilon \)’s the same quantity rather than two bounds that happen to share an \(\varepsilon \).

One reading of that quantity is the proposition’s, the other is its double. Under the search reading the property advantage is \(\Pr [\Win _{\op {Fin}}]\), so the left edge is already the transfer statement and no factor of two appears; under the decision reading the advantage is \(2\Pr [\Win _{\op {Fin}}]-1\), which doubles it. Every per-functionality property proof in the paper is an instance of this one square, which is why it earns a diagram where the instances do not.

Two things this buys. The hypothesis on the ideal side is now the property against the dummy alone — one statement about \(\sigma \), quantified over environments and nothing else — where Proposition 5.10 on its own asked for the property against the particular simulator the emulation supplied. Nothing need be assumed about how that simulator corrupts or leaks — only that it does not branch on a framework-internal refusal, which Section 4.4 asks of every machine it moves: whatever else it does, absorbing it into the environment turns it into part of a machine the ideal-side hypothesis already covers. And the conclusion is the property of the real system against every adversary, not only against the dummy, by the same move applied on the other side. Read concretely, the two absorptions are the whole price: for an \(\bd {a}\)-bounded \(\Adv \) and an \(\bd {s}\)-bounded \(\Sim \) the innermost statement is reached at environment budget \(\bd {z} \oplus \bd {a} \oplus \bd {s}\), one hosting cost per machine moved, and Chapter 8 charges nothing else.