Chapter 1
Functionalities and Systems

We work in the universal composability framework of Canetti [7], several of whose conventions we make explicit below.

A process id names a running protocol instance, and it has three parts:

a functionality name \(F\), a session id \(s\), and an instance number \(i\). The name says what code runs, the session which run of a protocol the instance belongs to, and the number distinguishes several instances of one name within a session. We write \(\id .F\), \(\id .s\) and \(\id .i\) for the three parts of \(\id .\PID \), and likewise \(\F .F\), \(\F .s\), \(\F .i\) for those of \(\F .\PID \); a bare \(\id .\PID = \F .\PID \) means all three agree.

Names are elements of \(\bits \cup \{A,Z,C\}\) and party ids of \(\bits \cup \{A,Z\}\), where \(A\), \(Z\) and \(C\) are reserved for the adversary, the environment and the corruption register. Being reserved, none of the three is an element of \(\bits \), so a field declared to contain \(\bits \) contains none of them; and \(C\) names no party, the register being a machine that parties call rather than one any party runs. Each of the three runs as a single instance in a single session, fixed to be session \(0\) and instance \(0\), so their process ids are \((A,0,0)\), \((Z,0,0)\) and \((C,0,0)\). We abbreviate these to the bare names \(A\), \(Z\) and \(C\) throughout, the other two components carrying no information.

Tests are almost always on the name alone. Where we write \(\id .F = A\) we mean the name component, never the whole triple, and the same for \(Z\), for \(C\), and for any functionality named in a membership test.

Two of the fields below collect names of this kind, and they collect different things. A party set holds party ids, elements of \(\bits \cup \{A,Z\}\); a caller set holds whole process ids, because who may call is a question about instances and not only about code. A caller set is therefore written with the abbreviations

for the process ids of the adversary, of the environment, and of everything standard. Where an older notation would have admitted “\(A\) and \(Z\)” it now admits \(\Apid \cup \Zpid \), of which only \((A,0,0)\) and \((Z,0,0)\) ever occur, the execution supplying one of each; where it admitted “\(\bits \)” it now admits \(\Stdpid \), and there every session and instance genuinely does occur. Party sets keep the bare \(\{A,Z\}\), those being party ids and not process ids, so a declaration that once read \(\Ps := \admits \) has to be split.

A functionality is named the same way, by its name component written as a subscript: \(\Fsig \) is a functionality with \(\Fsig .F = \op {Sig}\), its session and instance left implicit, so the notation stands for a process id \((\op {Sig},s,i)\) with \(s\) and \(i\) unspecified. Where a particular instance is meant they are supplied separately; where only the code matters, they are not written at all.

Little is lost by suppressing them, because a functionality’s own code hardly ever reads them. Local or global, a core is written for the party it serves and the state it keeps; which session it belongs to, and which instance of its name it is, are the execution’s business rather than its own. In this paper \(s\) occurs in three places only — line 3 of \(\opl {Guard}\), the wrappers that invoke it, and the static check of Definition 1.3 — and \(i\) is never read at all. The instance number earns its place another way: it is what lets two instances of one name in one session carry the distinct process ids that Definition 1.2 asks for. Chapter 7 makes the observation into a statement: renaming sessions and instances is an isomorphism of executions, and an emulation proved at one process id holds at every other, under a hygiene condition on who may be called across sessions that every functionality here meets.

Identity sets say two things: which identities a collection of functionalities occupies, and which a machine may claim. The five fields recur in the parameter line of every box below, written without the owner’s name since the box heading supplies it. Only the first two fix \(\IDs (\F )\): the process id is shared by all its identities and the served parties supply the second component.

The fourth field records dependence. An entry of \(\F .\uses \) is a pair \((\F ',R)\): \(\F '\) names a functionality that must be present for \(\F \) to run, and \(R\) is a predicate saying what \(\F \) requires of whatever is found there. Naming a subroutine is rarely enough on its own — a subroutine that served none of its caller’s parties, or admitted none of its callers, would be useless — so we write

for the requirement that comes up most: \(\G \) serves every party \(\F \) serves, and admits \(\F \) among its callers. Without the second conjunct \(\opl {Guard}\) would refuse every call from \(\F \) to \(\G \).

What \(\uses \) records is what the code of \(\F \) names. The calls its wrapper makes on its behalf — to \(\Corr \) on lines 2 and 6 of Section 3.5, and to \(\Adv \) through \(\opl {Mediate}\) — are common to every standard functionality and are left out, which costs nothing: both targets serve \(\bits \cup \{A,Z\}\) and admit \(\Stdpid \), so \(\serves (\F ,\Corr )\) and \(\serves (\F ,\Adv )\) hold of every standard \(\F \) whatever its own fields, and an entry for either could never fail.

A system is what a protocol designer writes down — we use protocol and system interchangeably, ideal and real naming styles of writing one (below), not disjoint classes. Three machines are no part of it: the environment \(\Zenv \), the adversary \(\Adv \), and the corruption register \(\Corr \) of Section 3.1. None is standard, so by Definition 1.2 no system contains any of them and \(\IDs (\Zenv )\), \(\IDs (\Adv )\) and \(\IDs (\Corr )\) lie outside every system; the execution of Section 3.6 supplies all three instead. For \(\Zenv \) and \(\Adv \) that is what lets each claim its own identity while silenced on the system under test. For \(\Corr \) it keeps the register clear of the set operations of Section 4.1 and Chapter 6: no blocker is built for it, no replacement moves it, and every comparison runs over one and the same register. Reserving the three names also keeps them out of every \(\F .\admits \) declared as \(\Stdpid \), so no functionality admits the register among its callers — which is right, the register being a callee only.

Distinctness of process ids does real work. A system is determined by what it places at each id it uses, so membership is settled by the id alone. And every identity records that id in its first component, so distinct members have \(\IDs (\F ) \cap \IDs (\F ') = \emptyset \): the union above is disjoint, and no identity of a system is occupied twice.

Three things about this. The conditions on \(\G \) are exactly those \(\opl {Guard}\) imposes when the call is placed — name admitted, session matching unless the callee is shared, fields fitting — so \(\WF (\pi )\) says precisely that the calls the members of \(\pi \) are built to make can succeed. Matching is by name, not by the functionality itself, which is what lets a dependence survive subsystem replacement: an entry naming \(\varphi _q\) is met by whatever sits at that name, ideal or real, so long as it meets the rest. And the requirement half ties the fields of caller and callee together; \(\WF \) would say almost nothing without it.

Both quantifiers range over \(\pi ^{+}\), and each enlargement earns its place: on the right it makes an entry naming one of the three supplied machines satisfiable at all, none being a member of any system, and on the left it checks their own entries — immediately here, since \(\serves (\Zenv ,\Adv )\) and \(\serves (\Adv ,\Zenv )\) hold and \(\Corr .\uses \) is empty. What \(\WF \) does not do on its own is survive the constructions that follow: adding members could introduce obligations, and replacing a subsystem re-evaluates every requirement at the new occupant. Proposition 6.4 (Chapter 6) settles the first and Theorem 4.4 the second.

Conditions, collected.  Well-formedness is one of several static conditions this paper puts on systems, cores and machines, and they are defined where each is first needed — which leaves a reader no way to see which result reads which. The table collects them once. None of them is read during an execution: \(\opl {Exec}\) reads fields, not conditions, as Proposition 7.7 records for \(\uses \) in particular.

Two things the table makes visible. The first two rows share a name and are different conditions: \(\WF \) is about a system on its own, well-formed replacement about where an incoming system lands. And \(\WF \) and session-uniformity are duals — the calls a member is built to make, against who may reach it — which invites folding them into one condition. They are kept apart because no result needs both, and because one definition could not carry both anyway: the game of Definition 5.1 is required to be well-formed and is deliberately not session-uniform, as Remark 5.6 explains.

We say \(\F \) is local if \(\F .\admits = \{\PID : \PID .F = F^{\parent }\}\) for a designated parent (caller) name \(F^{\parent }\). (We leave it to the functionality to say whether \(\Apid \) and \(\Zpid \) may call it.) Intermediate notions are possible: a setup reachable from two named protocols admits \(\{\PID : \PID .F \in \{F_1,F_2\}\}\); and an \(\admits \) may pin whole process ids rather than names, listing its callers’ occupied instances outright — Remark 6.5 says why the private members of a realization should. At the other end we say \(\F \) is global, in the sense of generalized UC’s shared setup [8], if

one notion and not two: the first disjunct is the ordinary case, any standard functionality may call it, and the second covers the three machines the execution supplies — and whatever stands in their slots — global for a different reason and treated so wherever \(\op {global}\) is tested.

The distinction is what the session component is for. A local functionality is part of one run of one protocol, so a call may reach it only from its own session: line 3 of \(\opl {Guard}\) asks \(\id '.s = \id .s\). The instance number is not checked, so one session may hold as many instances of a name as it likes and they may call one another. A global functionality is shared across runs — one session of it, reachable from every session — so that check is waived for it, and the sessions of \(\F \) may all call one shared instance. We name a global ideal functionality with a leading \(\op {G}\) and a global real one with a leading \(\gamma \), as in \(\F _{\op {G}\op {Sig}}\); the calligraphic \(\G \) stays what it has been, a second functionality alongside \(\F \). The three machines the execution supplies are global: \(\Adv \) and \(\Corr \) already by the first clause, and \(\Zenv \) by the second, which is there because \(\Zenv .\admits = \Apid \cup \Zpid \) is deliberately narrow and yet the environment must be reachable from every session.

Real vs. ideal specifications.  Ideal functionalities and real protocols differ in several respects. First, ideal functionalities know the corruption status of parties in their party sets. Second, they can pass the execution to the simulator and may offer simulator-specific interfaces (see, e.g., \(\Fdiffuse \)). Finally, they may share state across parties — and sharing is the point: the guard of Chapter 2 ties every call to one party, so parties communicate only through functionalities that share state across them, and a real protocol talks to its peers through ideal subroutines and in no other way. Here and below, \(\Fdiffuse \) and \(\Fio \) name functionalities we do not give: a diffusion channel and an input–output relay. Nothing in this paper depends on their code. The randomness source \(\Frand \) and the store \(\Fstore \) are given, in Chapters 13 and 14; they are the smallest examples in the paper and are where a reader new to the style should start.

The core interfaces of well-specified real protocols have none of these features, beyond those implicit in idealized building blocks and access-control wrappers; and real realizations do not specify how leakage is computed upon corruption, it being the contents of work tapes.¹

Initialization.  \(\op {Initialize}\) is a procedure and not an interface: it runs once, when the functionality is first activated, and sets up the variables the rest of the code uses. It places no calls — the execution of Section 3.6 initializes every machine before its dispatcher is installed, so there would be nothing to serve one — no caller can reach it, it takes no claimed caller-id, and a functionality declaring none gets the empty one. Real protocols carry no global initializer of this kind, only ones specific to a party within a process, written \((\PID ,P).\op {Initialize}()\) and abusing notation: they are private, not interfaces anyone may address.