3.3 The Environment

We define a special functionality \(\Zenv \), with a single per-\(\id \) interface \(\id .\fopl {Z}\) that guards and silences the core \(\id .\op {Z}\). The field \(\Zenv .\admits = \Apid \cup \Zpid \) deserves emphasis: it admits the adversary and the environment itself and nothing else, so no standard functionality may call \(\Zenv \). Anything wider would let a protocol call the environment as one of its own subroutines — an “open protocol,” whose subroutines are left undefined. Two distinct things rule that out. The narrowness of \(\Zenv .\admits \) refuses the call itself: a standard caller’s process id lies in \(\Stdpid \), which meets \(\Apid \cup \Zpid \) nowhere, so line 2 of \(\opl {Guard}\) rejects it whatever the caller declares. Definition 1.3 refuses the other half of openness, a member naming a dependence no member supplies. It is the first that does the work here: naming \(\Zenv \) would not trip \(\WF \), since \(\Zenv \in \pi ^{+}\) makes such an entry satisfiable, so a system could be well-formed and still be open were the field any wider.

The \(\Zpid \) in \(\Zenv .\admits \) is there for a different reason: it lets \(\Zenv \) call itself. The \(\op {Z}\) interfaces of the environment at different parties are separate, and admitting \(\Zpid \) is what lets them reach one another.

Which of them may reach which is settled by the silenced set, and there it does more than keep \(\Zenv \) off the systems. Every other machine is tied to where it runs: a standard functionality may claim only its own identity, and \(\Adv \) is silenced on \(\{\id '' \neq \id \}\). Nothing would tie \(\Zenv \) on its own, since \(\opl {Silence}\) tests only the claimed \(\id '\) and \(\opl {Guard}\) only the target, so \((Z,P)\) and \((Z,P')\) would be interchangeable and the party component of a \(\Zenv \) identity would carry no information. Line 3 supplies the tie, as loosely as applications allow: an interface at \(\id \) may claim \(\id '\) when \(\id '.P = \id .P\), when \(\id '.P = Z\), or when \(\id .P = Z\). In words, act for your own party, or for the root; and the root may act for anyone.

Both escapes are needed. Without \(\id .P = Z\) the root is stranded, and it is where \(\opl {Exec}\) begins and the only interface that can reach the others. Without \(\id '.P = Z\) the leaves are: the adversary’s only route back into the environment is \((A,P) \to (Z,P)\), and \(\opl {Mediate}\) wakes \(\Adv \) at \((A,\id .P)\) for the party it answers for, so an environment needing to compare what the adversary said at \(P\) against what it said at \(P'\) could never bring the two together — these interfaces are separate, and cannot pool it through shared state either — and the class of Definition 4.11 would genuinely shrink. With both escapes, connectivity is a two-way star rooted at \((Z,Z)\), and we know of nothing an unrestricted environment could do that the star cannot. Line 2 restricts in the same spirit: it stops \(\Zenv \) claiming \((A,P)\), and so stops it passing the corruption gate of line 3 and driving an honest party’s interface — a capability the adversary it would be impersonating does not have either, as Remark 4.8 records of a simulator silenced on less. What that line no longer has to do is keep \(\Zenv \) away from \(\fopl {Corrupt}\), which line 3 admits it to under its own name.

Together, \(\Apid \cup \Zpid \) is what applications need and no more. Admitting \(\Apid \) is necessary because the environment has no other way back into the execution: once \(\Zenv \) passes the token on it runs again only when something calls it, and only the adversary may; that same channel is how \(\Zenv \) hears whatever the adversary chooses to tell it. Admitting \(\Zpid \) is necessary because the environment is one interface per party rather than one machine, and without it the root could reach none of them. Nothing beyond these two is: a functionality that had to call \(\Zenv \) would treat it as a subroutine it does not define, and \(\Corr \) reports corruptions to no one — the adversary knows what it corrupts, having done it — which is why \(\Zenv \) must ask for the corruption set. So the environment is reachable only from the two machines outside every system.