4.4 Completeness of the Dummy Adversary

The dummy adversary carries out whatever the environment tells it and reports back whatever it is told; it has no strategy of its own. Anything a real adversary achieves, an environment can achieve by driving the dummy, which is why quantifying over adversaries can be replaced by quantifying over environments. This section defines it and proves that, for the systems and classes the theorem makes precise — Remark 9.4 records the one regime, cores placing responsive calls, that the claim does not reach.

What the framework already fixes.  The dummy is not a new kind of machine. It is the adversary of Section 3.4 with a particular core, so it carries \(\Adv \)’s fields and its calls pass through \(\Adv \)’s wrapper. Three consequences settle the shape of the code before a line of it is written.

First, it may claim one identity only. Line 2 of the \(\Adv \) box silences a core on \(\{\id '' \ne \id \}\), so every call the dummy places claims \(\id \), the identity it runs at. An instruction of the form “call \(\id ''.\Op \) as \(\id '''\)” therefore cannot be carried out for an arbitrary \(\id '''\): the dummy speaks as \((A,\id .P)\) or not at all. What the environment chooses is not the claimed id but the party, by instructing the dummy at \((A,P)\) rather than at \((A,Q)\); the root of \(\Zenv \) may act for any party and so may pick either.

Second, the party of the target is forced. The predicate \(\opl {Guard}\) asks \(\id '.P = \id .P\) of the callee, and the claim is \((A,\id .P)\), so the dummy at \((A,P)\) reaches interfaces of party \(P\) and no other. A target that does not admit \(\Apid \), or an honest party, refuses the call by line 2 or line 3; the dummy passes the refusal back, and the rule of Section 3.6 delivers it to the dummy’s own caller as \(\none \).

Third, its route to the environment is fixed too: \((A,P) \to (Z,P)\), which \(\opl {Guard}_{\Zenv }\) admits because \(\Apid \subseteq \Zenv .\admits \) and the parties agree.

The code.  The core dispatches on who called it. A call from the environment is an instruction to carry out; a call from anything else — a mediation hook, or an \(\Adv (\cdot )\) placed inside some core — is a message to hand on. In both directions the payload has the shape \(\opl {Mediate}\) already uses, an operation together with a value.

Line 3 is the outward direction: the environment names a target interface and an input, and the dummy places exactly that call and returns exactly its answer. Nothing is inspected and nothing remembered — the dummy keeps no state, so it has no \(\op {Initialize}\). Line 5 is the inward one: whatever reaches the adversary is handed to the environment together with the identity it came from, and whatever the environment answers is returned to that caller unchanged. The two lines are the same relay read in opposite directions, which is what makes the dummy transparent.

An instruction line 2 cannot parse is answered with \(\none \): the guards answer anything the dummy cannot place with \(\rej \), but a payload that names no call at all needs a value of its own, and \(\none \) is what a machine with nothing to say returns.

One detail is worth pausing on. The caller \(\id '\) is passed to \(\Zenv \) on line 5 and not merely the payload: without it the environment could not tell which interface is asking, and a relay that loses that cannot be transparent.

Interposing an adversary.  Completeness is a statement about moving an adversary from the execution into the machines around it, and needs a name for each move. Both are the same operation seen from two sides: \(\Adv \) is placed between some machine and the dummy interface, so what used to reach \(\Adv \) now reaches it inside, and what \(\Adv \) used to place now leaves as an instruction to \(\Dum \).

Neither construction is a new kind of machine. The bundle \(\Zenv ^{\Adv }\) occupies what an environment occupies and claims what \(\Zenv \) claimed, so it is admissible exactly when \(\Zenv \) is. It occupies no \(A\)-identity, those being the relay’s in the right-hand execution, so by Definition 4.13 the hosted \(\Adv \) has no identity of its own to place a call under: hence the rewriting above, and hence the obligation — discharged by Siting below — to check the rewritten claim against \(\Zenv \)’s silencer. Absorption in Chapter 4 is the other case of Definition 4.13, which is why a hosted functionality there keeps its claim instead. Meanwhile \(\Sim [\Adv ]\) occupies \(\IDs (\Adv )\), which is what standing in the adversary slot means.

The theorem.  Emulation with respect to the dummy alone is Definition 4.11 with the adversary class cut down to the single machine \(\Dum \). The claim is that nothing is lost.

One mild condition on the adversary is needed, and it is the price of the dummy being a relay.

The dummy relays such an answer, and by Section 3.6 its own return of a \(\rej \) reaches the caller as \(\none \); so where an unabsorbed adversary placing a refused call reads \(\rej \) directly, the same adversary driving the dummy reads \(\none \). A refusal-oblivious adversary cannot tell the two apart, which is what the regrouping below needs. The dummy is itself refusal-oblivious — it relays its answer without branching on it — so the hypothesis costs the dummy class nothing, and a real adversary that reads a framework-internal refusal signal is in any case a modelling artefact rather than an attack.

Informally, Theorem 4.29 says that emulation with respect to the dummy alone loses nothing: anything a real adversary achieves, an environment can achieve by driving the dummy, and the simulator for \(\Adv \) is \(\Sim _{\Dum }[\Adv ]\) — the one simulator the hypothesis supplies, with \(\Adv \) interposed before it — which depends on \(\Adv \) alone and not on \(\Zenv \).

Diagrammatically, the proof is the same commuting square as Theorem 4.20’s (the figure above its proof), built this time from the ceding half of Lemma 4.18 rather than the keeping half: what moves into \(\Zenv \) is not part of the system but the adversary itself, and a relay stands where it stood.

Bottom left is where the theorem starts: \(\pi \) and \(\varphi \) untouched throughout, \(\Adv \) the real-world occupant and \(\Sim _{\Dum }[\Adv ]\) — \(\Sim _{\Dum }\) with \(\Adv \) interposed before it — the derived ideal-world one. The top and bottom edges are (R1) and (R2) of the proof: absorbing \(\Adv \) into \(\Zenv \), on whichever side it is read, is again an equality of distributions, exactly as Proposition 4.19’s was — but this time it is the ceding half of Lemma 4.18 paying for it, hypotheses (a)–(c) in place of nothing, because what moves is the adversary itself and a relay (\(\Dum \), then \(\Sim _{\Dum }\)) has to stand in its place. The same absorbed \(\Zenv ^{\Adv }\) serves both sides, which is why the right edge can compare them at all: it is the theorem’s hypothesis, stated only against \(\Dum \). Chasing the square exactly as in Theorem 4.20, the left edge — the theorem’s conclusion, now for every refusal-oblivious \(\Adv \) rather than one fixed machine — is forced: the two \(\approx _\varepsilon \)’s are, by the two equalities, the same quantity.

The three classes move as in Theorem 4.20, and for the same reasons. The adversaries are those the conclusion quantifies over, and the hypothesis had only \(\Dum \); the simulators are computed, one per adversary, by interposing it before the simulator the hypothesis supplies; and the environments are a preimage, an outer \(\Zenv \) counting exactly when what it becomes on absorbing each \(\Adv \) is one the hypothesis covers. Taking \(\ZenvSet \) to be the largest admissible class makes \(\ZenvSet '\) the largest one again — less only the environments that silence their own \(Z\)-identities, a condition no admissibility imposes and no application wants, excluded because the instruction of Definition 4.26 leaves under a \(Z\)-claim, which such an environment would refuse on one side alone — since absorption leaves \(\pars \) alone.

Read concretely in the sense of Section 4.5, the two constructions cost what the adversary costs: if \(\Adv \) is \(\bd {a}\)-bounded then \(\Zenv ^{\Adv }\) needs \(\bd {z} \oplus \bd {a}\) where \(\Zenv \) needed \(\bd {z}\), and \(\Sim _{\Dum }[\Adv ]\) needs \(\bd {s} \oplus \bd {a}\) where \(\Sim _{\Dum }\) needed \(\bd {s}\). The invocation counts add and the per-invocation times take a maximum, both independent of \(\pi \) and \(\varphi \).