4.2 Emulation and Absorption

Everything an execution needs is now fixed, so we can say when one system is at least as secure as another. The two are placed under one and the same environment, so what it may claim must be settled first; that is the role of \(\Zenv .\pars \) below.

The value of \(\opl {Exec}(\pi ,\Zenv ,\Adv ,\Corr )\) is whatever the environment returns. We take an environment to return a bit at the root — its guess as to which system it was placed in — and read the execution as returning \(1\) exactly when the environment does. Nothing else in the framework constrains that value, so this is a condition on the environments quantified over, not a consequence. The gap between two executions is then a number, not an informal resemblance.

The two executions differ in the system and in the machine that occupies the adversary’s identities: \(\Adv \) on one side, \(\Sim \) on the other. Both are typed by the same pair of definitions.

Every simulator is thus an adversary, which is what lets one stand in an adversary class: Proposition 4.12 and Theorem 4.24 read simulators as adversaries, and the budget containments of Section 4.5 compare the two classes directly. Occupancy and the admitted callers are what standing in the adversary’s slot means, so everything Section 3.4 settles about a machine at \((A,P)\) holds of a simulator unchanged: it begins no call of its own, and its silencer lets it claim only the identity it runs at. Proposition 4.19 asks only occupancy of whatever it is given; Theorem 4.29 uses the wrapper and the admitted callers too, and Remark 4.8 explains why neither is a restriction.

The metric takes the three machines as arguments, so emulation can be stated by quantifying over classes of them and bounding the result. Which environments may be used at all is settled by the pair being compared.

The second condition is occupancy hygiene: an execution is defined only for occupants with pairwise disjoint identity sets (Definition 3.3), so an environment hosting at an identity one of the systems occupies could not be placed beside it, and admissibility rules it out for both worlds at once.

The containment is justified below. A statement of emulation then fixes three classes: a class \(\Aset \) of adversaries (Definition 4.6), a class \(\SimSet \) of simulators (Definition 4.7), and a class \(\ZenvSet \subseteq \ZenvSet _{\pi ,\varphi }\) of environments (Definition 4.9). Taking \(\ZenvSet = \ZenvSet _{\pi ,\varphi }\) gives the strongest statement of the three, and is the default reading.

The order of the quantifiers is the substance of the definition: the simulator may depend on the adversary but not on the environment, so one \(\Sim \) must work against every \(\Zenv \in \ZenvSet \) at once. Otherwise the two executions are one experiment with a single system swapped, \(\Zenv \) being literally the same machine on both sides. Weakening it to \(\forall \, \Adv \ \forall \, \Zenv \ \exists \, \Sim \) — a simulator built for the environment it faces — gives a notion Definition 4.11 implies and whose converse we do not prove, the two reading as \(\max _\Adv \min _\Sim \max _\Zenv \) and \(\max _\Adv \max _\Zenv \min _\Sim \) of one quantity in the concrete form of Section 4.5. The composition results survive the weakening, each proof below instantiating the hypothesis at an environment fixed by the conclusion’s; what the order buys is therefore meaning rather than composition, since only under it is \((\varphi ,\Sim )\) one system behaving like \((\pi ,\Adv )\) whoever is watching — an ideal world one can name and hand on.

Definition 4.10 is what makes the comparison meaningful. Since \(\Zenv .\pars \) silences \(\Zenv \), it may claim no identity inside it, and three kinds must be kept out of reach. An identity in \(\IDs (\pi ) \mathbin {\triangle } \IDs (\varphi )\) is occupied in one world and free in the other, so an environment allowed to speak as one is told which world it is in before anything happens, and no simulator can repair that. An identity internal to both separates nothing, but an environment claiming it speaks as a component of the system rather than from outside, which an environment is not for. And an unoccupied identity of a used name is as good as an occupied one, because \(\opl {Guard}\) admits callers by name: a local callee admits every instance of its parent’s name, line 2 asking no more, so an environment claiming a fresh instance of that name drives internal subroutines exactly as their callers do — and against a blocked pair (Chapter 6) it tells the worlds apart outright, the blocker refusing a call the genuine occupant admits. Silencing the closure disallows all three at once. What stays claimable is fresh names, and those reach only what admits all of \(\Stdpid \): the global functionalities, shared between the two worlds in any comparison where they are not themselves at issue.

Silencing governs what \(\Zenv \) may claim, and calling is a second channel it does not touch. An identity of \(\IDs (\pi ) \mathbin {\triangle } \IDs (\varphi )\) may be called in either world: where nothing occupies it the answer is \(\rej \) (Section 3.6), and where something does the answer is \(\rej \) again — provided that something refuses \(\Zpid \) at line 2. The proviso is a condition on the systems being compared rather than on the environment class, and a pair breaking it is simply not emulable, no simulator being able to invent an answer the ideal world has no machine to give. It is why the local subroutines of Chapter 20 keep \(Z\) out of their \(\admits \).

Smaller sets being less restrictive, the least restricted admissible environments are those whose \(\pars \) is the closure exactly — and the blocking of Chapter 6 delivers them for a compatible pair:

by the second claim of Theorem 6.3, and a blocker copies its name from the member it stands in for, so

So \(\Zenv .\pars := \ncl {\overline {\pi }}\) is not merely a value the two blocked systems can share, but the weakest restriction the pair admits.¹

One property of the relation is already available, and it is of a different kind from everything that follows. The composition results below — substitution, parallel composition, the completeness of the dummy adversary — are corollaries of a single absorption lemma, each regrouping one execution and reading the same advantage twice. Transitivity regroups nothing. Its proof is the triangle inequality over Definition 4.5 together with the check that the conclusion’s class is admissible for the outer pair, so it belongs to the metric rather than to the machinery and needs none of the apparatus of the rest of this section. It is stated here for that reason.

Three constructions below — the absorbed environment here, and the two of Section 4.4 — fold several machines into one occupant of the execution. They share a shape, which we name once.

That internal traffic is served rather than placed is what lets a bundle occupy the adversary slot of a system whose cores call it responsively, and it is worth saying why the distinction is not a quibble. The wrapper \(\opl {Respond}\) (Definition 9.1) refuses every call the responder places, so a bundle obliged to place its internal calls could reach none of its own members while answering one — and the simulator of Chapter 20, which drives three hosted hybrids inside each of two responsive answers, could not run at all. Serving them inside leaves the token where it was, which is the whole of what responsiveness asks. What a bundle still may not do inside a responsive answer is reach anything it does not host: the register and the shared functionalities are outside it, so their calls are placed, and refused.

Definition 4.13 already says that a hosted machine comes in two kinds, according to whether the bundle occupies its identities, and the difference is the whole of what follows. A machine whose identities the bundle keeps disappears from the execution’s dispatch and is served inside; one whose identities the bundle cedes must leave them to somebody, and its calls must be placed by that somebody on its behalf. Both moves come up — the first absorbs a protocol, the second an adversary — so we define them together and prove them right once.

We state the ceding case for the adversary slot alone. It is the only one used below, and the only one whose interface has an instruction shape to rewrite calls into — a standard functionality serves what its own code names and could not stand in for another machine’s calls.

Both halves of the outward set are forced by what the absorbed execution has to reproduce. The first is the slot, whose identities go to \(\pi \) or to \(\varphi \) according to which world the absorbed environment sits in. We take the union rather than \(\IDs (\varphi )\) alone so the same machine serves in both, which matters now that the two need not occupy the same identities. The second is the two reserved ids \(A\) and \(C\), named as ids rather than as machines because the adversary slot holds \(\Sim \) on the ideal side while Proposition 4.19 needs one and the same absorbed machine on both. They are there because the hosted machines are full interfaces rather than bare cores: each reads the register on lines 2 and 6 of Section 3.5, and each hands a call at a corrupt party to the adversary through \(\opl {Mediate}\), which hooks to \((A,\id .P)\). Neither id belongs to any system. Without this half a call to a hosted functionality would be refused at its first line, and a corrupt party’s hook would be refused instead of reaching the adversary: the absorbed execution would stop being the outer one regrouped exactly when \(\Cs \) met \(\rho \setminus \varphi \). Everything else is answered with \(\rej \), nothing serving it in the outer execution either.

The parameter is carried over untouched, and it must be. It is the silenced set of \(\Zenv \)’s own interface, so any change to it changes which calls \(\Zenv \) may place — and \(\Zenv \) is the one machine that has to behave identically on both sides. One might think the hosted functionalities need \(\IDs (\rho \setminus \varphi )\) removed from it to speak as themselves, but they do not: each is a full interface, and line 5 of its own wrapper is what licenses its claim, \(\Zenv \)’s reaching no further than \(\Zenv \)’s own core (Definition 4.13). Removing those identities would licence nothing new for them, and would un-silence \(\Zenv \) on exactly the identities it was silenced on before absorption.

Absorbing thus turns an environment for the outer pair into one for the inner pair, preserving admissibility. The register needs no special treatment: being a member of no system it lies in neither \(\varphi \) nor \(\rho \setminus \varphi \), so the absorbed environment does not host it and blocking builds no blocker for it. Like \(\Zenv \) and \(\Adv \) it is supplied by \(\opl {Exec}\), the same single machine on both sides of every comparison. Its hosted copies keep their identities, so by Definition 4.13 they leave their calls under their own claims and meet their own silencers — not \(\Zenv \)’s — which is what the regrouping below needs; the constructions of Section 4.4 are the opposite case, hosting an adversary whose identities the bundle does not occupy.

What makes the theorem work is that absorption regroups an execution without changing it. Since the same correspondence serves Section 4.4, we set it down before the lemma.

Configurations.  By a configuration of an execution we mean its state between activations: the state of every machine, the unread part of every coin tape, which machine holds the token and where in its code, and the callers suspended awaiting answers. Calls nest, and Section 3.6 lets an instance hold several outstanding continuations, so the last of these is a chain rather than a set: one entry per call placed and not yet answered, in the order placed, recording the caller and the call it waits on.

The two executions do not run the same machines — that is what absorbing does — but they run the same ones once \(\Zenv ^{H}\) is counted as the machines it bundles rather than as one, and but for the relays a ceded identity needs. Definition 4.13 passes the token among those as \(\opl {Exec}\) does, so each holds it in the same sense on either side. Counted so, the machines of the two executions correspond one to one apart from the relays, and we write \(\iota \) for the bijection: the hosted copy of each member of \(H\) to that member, the hosted \(\Zenv \) to \(\Zenv \), and everything the execution still runs, \(\Corr \) included, to itself.

Only (C4) is at risk from the bracketing. On the left every suspension is recorded by \(\opl {Exec}\); on the right they divide between \(\opl {Exec}\) and the bundle, which records those of the calls internal to it. The clause asks that the two chains agree once the bundle’s own are counted where they were placed. Regrouping is exactly that: one chain of suspensions, kept by two dispatchers.

The first activation.  The two executions begin in correspondence, and it is worth saying why, since this is the one activation the lemma’s case analysis does not reach: it is placed by no machine. Line 1 initialises \(\Corr \) and everything the execution still runs on both sides, Definition 4.14 initialises each hosted copy as \(\opl {Exec}\) would, and a relay carries no state, so every machine and its image start in the same state, which is (C1). No tape has been read, giving (C2). The operation \(\op {Initialize}\) places no calls, so nothing is suspended and both chains are empty, giving (C4) — and with it the reason the order in which the bundle initialises its copies cannot be observed: that order can be read off nothing in the configuration. Line 2 then activates \((Z,Z).\fopl {Z}()\) from \((Z,Z)\). On the left the token goes to \(\Zenv \); on the right it goes to \(\Zenv ^{H}\), where \((Z,Z)\) is carried by the hosted \(\Zenv \), which Definition 4.14 makes the bundle occupy. Both enter \(\fopl {Z}\) at the same identity on the same input, which is (C3).

Thereafter every activation is a call placed or a value returned, and the lemma comes to showing that correspondence survives one of them on either side, and that corresponding configurations halt together with the same output. Its paragraphs take those activations case by case.

Diagrammatically, the lemma is one equality with its two cases side by side: a kept member disappears into the bundle outright, a ceded one is bridged back out through a relay.

A member of \(H_{\op {keep}}\) — like all of \(\rho \setminus \varphi \) in Theorem 4.20’s figure above — is absorbed outright: \(\Zenv ^{H}\) occupies its identity, so \(R\) reaches it only as part of the bundle. A member of \(H_{\op {cede}}\) is hosted too, running on the same tape, but the bundle does not occupy its identity: the relay \(\Dum \) (the dummy of Section 4.4) stands in its place, handing \(R\)’s calls to \(\Zenv \) tagged with their caller and re-emitting the hosted member’s outward calls under its original claim, so neither side can tell a relay sits between them. Hypotheses (a)–(c), asked only of \(H_{\op {cede}}\), are what keep that indistinguishable: (a) is exactly refusal-obliviousness, since \(\Dum \) turns every \(\rej \) it relays into a \(\none \); (b) and (c) rule out a responsive call and a clash on \(\Zenv \)’s own claim, the two other ways a relay’s extra hop could show. Theorem 4.20’s figure is the case \(H_{\op {cede}} = \emptyset \); the mirror case, one ceded occupant standing for the whole adversary slot (\(H_{\op {keep}} = \emptyset \)), is what Section 4.4’s dummy-adversary construction runs on.

The two halves of the lemma are used apart. Absorbing a protocol cedes nothing, so all three hypotheses fall away and what is left is a pure rebracketing; that is the case Theorem 4.20 runs on, and it is worth stating separately for the emphasis that it costs nothing at all.

The theorem now says that substituting one subsystem for another inside a protocol costs nothing in advantage.

Informally, Theorem 4.20 says: if \(\pi \) UC-emulates \(\varphi \) within \(\varepsilon \), then \(\rho [\pi /\varphi ]\) UC-emulates \(\rho \) within the same \(\varepsilon \). The adversary and simulator classes carry over unchanged; the environments of the conclusion are those admissible for the pair \((\rho [\pi /\varphi ],\rho )\) whose absorbed form \(\Zenv ^{\rho \setminus \varphi }\) lies in the class of the hypothesis.

Diagrammatically, fixing one \(\Adv \in \Aset '\), a serving \(\Sim \in \SimSet '\) and one \(\Zenv \in \ZenvSet '\), the proof is the commuting square below, drawn in the string-diagram style of [9]: a solid box is a system, a wire is an interface, and the box hanging off the bottom of a system is whichever machine currently occupies its adversarial slot.

The top and bottom edges are Proposition 4.19, applied to \((\pi ,\Adv )\) and to \((\varphi ,\Sim )\) respectively — regrouping is free, so both are equalities, not mere bounds, which is why the dashed box on the right (the absorbed environment \(\Zenv ^{\rho \setminus \varphi }\) of Proposition 4.19) is the only thing that changes between a column and its neighbour. The right edge is the theorem’s hypothesis, applied to that absorbed environment. The left edge — the theorem’s conclusion — is then forced: chasing the square shows the two \(\approx _\varepsilon \)’s are not merely both bounded by the same \(\varepsilon \) but, by the two equalities, are the very same quantity. Composing \(n\) such squares in a chain, one hybrid at a time, is exactly Theorem 4.24 below.

Substitution and transitivity now combine into the form in which composition is actually used. Proposition 4.12 was stated with the metric above, its proof needing none of this machinery; here is where it does its work.

This is the form in which composition is used. One analyzes \(\rho \) with the idealized subroutine \(\varphi \) in place, proving it emulates whatever specification \(\psi \) is wanted — against the classes the corollary names, whose adversaries are the first step’s simulators; the corollary transfers that conclusion to the system that runs. One hypothesis is easy to miss: emulation against \(\ZenvSet '\) asserts, as Definition 4.11’s side condition, that \(\ZenvSet ' \subseteq \ZenvSet _{\rho ,\psi }\) — so \(\psi \)’s names must lie under the \(\pars \) of every environment the class retains, and the corollary is vacuous where they do not.