Universal composability is written, almost everywhere it is written, in a mixture of prose and code. A functionality’s interfaces are code; who may call them is a sentence. The corruption model is a paragraph; what a corrupt party’s interface actually returns is left to the reader. Each gap is small, and a human referee closes it without noticing. A machine cannot, which is why a UC proof is hard to falsify and harder still to check formally: much of what would have to be checked was never written down.
This paper writes those parts down as code. Identities and access control become data that a functionality carries in named fields. Wrappers enforce them: a guard decides which calls reach a core, a silencer decides what a core may claim, and a mediator hands a corrupt party’s call to the adversary. Corruption is a register that every interface reads, twice, at points the code names. An execution is a handler that passes a single token. Nothing here is a new model — it is Canetti’s [7], with several of its conventions made explicit — but stating them in code rather than prose is what lets the rest of the paper be proved rather than argued.
One lemma. Emulation is then defined over explicit machine classes, with concrete bounds: no security parameter, no asymptotics, a bound that is a number. What follows is a composition toolkit, and the shape of it is the paper’s main structural claim. Substitution, parallel composition and the completeness of the dummy adversary are all corollaries of a single absorption lemma, which moves a protocol or an adversary into the environment. Absorption is not a comparison of two executions but an exact regrouping of one: the same run, bracketed differently, so the advantage on either side is the same number rather than two numbers with a shared bound. Transitivity is the exception and is of a different kind, resting on the triangle inequality over the metric rather than on any regrouping; it is stated with the metric for that reason, before the machinery the other three need.
Games are functionalities. A property in the game-based style of Bellare and Rogaway [5] — unforgeability, liveness, authentication — turns out to be expressible as a functionality too, with the game’s challenger as an ordinary machine and its verdict as an ordinary interface. Properties written this way transfer along emulation: if a protocol emulates an ideal object, the object’s properties descend to it, under hypotheses the paper states and checks at each use rather than assuming.
What to read first. The apparatus is larger than the theorem count suggests, and not all of it is load-bearing. Five definitions carry most of the paper: a functionality and its five fields; an execution and what it means to occupy an identity; a bundle, which runs several machines as one occupant and is what absorption is built from; absorption itself; and the regrouping correspondence that pairs two executions machine by machine. A reader who has those has the spine, and the composition results follow from them in order. The concrete functionalities — a signature scheme, a global clock and a bounded-delay network after Katz, Maurer, Tackmann and Zikas [11] and Badertscher, Maurer, Tschudi and Zikas [3], and an authenticated channel realized over them — come last and exist to show the style at work rather than to be needed by anything before them.
What this is for. A UC researcher should find the conventions here the ones they already use, written down. The second audience is the one the extra precision is for. Anyone building tools over UC — a type-checker for functionality code, a proof-assistant encoding, a test harness — needs a specification that settles the questions an informal presentation can leave to its reader, and settling them is most of what this paper does: which caller a guard admits, what a silenced core may claim, when a corruption register is read. Whether that is enough to carry a machine-checked UC proof is not established here, and we do not claim it. It is why the framework is written this way.