Chapter 2
Guards, Silencers, and Mediators

This chapter fixes three pieces of machinery. The predicate \(\opl {Guard}\) constrains the calls that reach a machine; the wrapper \(\opl {Silence}\) constrains the calls it makes; and the wrapper \(\opl {Mediate}\) hands to the adversary a call that a corrupt party cannot answer for itself. The full interface of Section 3.5 is their composition.

Write \(\Op \) for a generic core interface of \(\F \). We specify only the cores; the wrapper below turns each into a full interface, and a caller reaches \(\fopl {Op}\), never \(\Op \). The access control checks are collected in the predicate \(\opl {Guard}\), which is not a functionality but an algorithm: it takes the target identity \(\id \), the claimed caller identity \(\id '\) and the functionality \(\F \), and returns a boolean. Two conventions of presentation. Boxes come in two weights: a filled one marks a functionality, which occupies identities, and an unfilled one a predicate, wrapper or procedure, which occupies none. And a call is written \(\id .\Op (in)\) as \(\id '\) where \(\id '\) is the identity claimed in placing it, and received as \(\id .\Op (in)\) from \(\id '\) where \(\id '\) is the identity it was claimed under. Enforcement sits in the wrapper, where line 1 requires it, so a call it rejects never reaches a core. Line 1 checks that the interface exists; line 2, that the caller’s name is admitted and that it acts for the right party; line 3, that caller and callee lie in one session, unless the callee is shared across sessions.

\(\opl {Guard}\) constrains the calls that reach a machine; the wrapper \(\opl {Silence}\) below constrains the calls it makes. It takes an identity set \(\Ids \) and a programme, runs it, and intercepts every call it issues. A call claiming an identity in \(\Ids \) is refused with \(\rej \) without ever being placed; any other is placed and its answer handed back. So \(\Ids \) is exactly where the wrapped programme is silenced, and it may speak as anything outside.

The scope is the wrapped programme and nothing further. A call it places passes the token to another machine, and what that machine says is governed by its own wrapper, not by this one. Were it otherwise a functionality would silence its subroutines transitively, and none could speak as itself. Every use of \(\opl {Silence}\) below is of this shape: a full interface wrapping the core it serves.

It is convenient to read this as a handler, in the sense of algebraic effects [12, 4]. A call the programme issues is an operation of the ambient effect, and \(k\) is the continuation waiting for its answer. The wrapper \(\opl {Silence}\) decides what to resume with: \(\rej \) for a silenced claim, the answer of the call actually placed otherwise. The return clause passes the programme’s own result through untouched, so silencing changes what the programme may say and nothing else. The analogy only fixes the shape of the wrapper.

With \(\opl {Silence}\) in hand we can say what happens to a call that a corrupt party cannot answer for itself. Every full interface below hands such a call to the adversary twice, on the way in and on the way out, and both times in the same shape: the wrapper \(\opl {Mediate}\). It takes a corruption set \(\Cs \), the operation \(\id .\Op \) being served, the value \(x\) to hand over, and the claimed caller \(\id '\) of the operation it stands in. Where the answer comes from is fixed inside it: whatever the operation, a corrupt party’s answers come from \((A,\id .P)\). One thing about it is not an ordinary argument: both require and the return of \(\opl {Mediate}\) return from the operation in whose code they stand, not merely from the line itself. When \(\opl {Mediate}\)’s test fails it does nothing and that operation carries on.

The hook is an ordinary call on \(\Adv \)’s full interface, claiming the identity \(\id \) of the interface being served. It therefore meets \(\opl {Guard}_{\Adv }\), which it passes because the claimed party \(\id .P\) is the party of the target; and the answering adversary is confined by \(\Adv \)’s own silencer, which admits only \((A,\id .P)\). So while answering for \(\id .P\) the adversary may speak as itself at \(\id .P\) and as nothing else, and \(\opl {Mediate}\) needs no silencing of its own.