UC for Gamers
![[Picture]](main0x.svg)
| AI: | Claude Opus 5 (1M context) |
| Prompts: | Pooya Farshim |
| Reviewers: | Nobody |
| Date: | August 16, 2026 |
Universal composability is usually written in a mixture of prose and code, which makes UC research hard to falsify, and harder still to test or verify formally. Following the code-based style of property-based security, we set out a rigorous language for programming UC functionalities: identities and access control are data, wrappers enforce them, corruption is a register that every interface reads, and an execution is a handler passing a single token. Emulation is then defined over explicit machine classes with concrete bounds — no security parameter, no asymptotics — and the composition toolkit follows: substitution, parallel composition and a completeness theorem for the dummy adversary — all three corollaries of one absorption lemma, which moves a protocol or an adversary into the environment and is an exact regrouping of a single execution rather than a comparison of two — with transitivity coming free from the metric itself. Game-based properties turn out to be functionalities too, and they transfer along emulation. A signature functionality, a global clock and a bounded-delay network show the style at work. We hope this helps apply formal methods to UC, and ultimately give a formal UC proof.
Introduction
Introduction
1 Functionalities and Systems
2 Guards, Silencers, and Mediators
3 The Execution Model
3.1 Corruption
3.2 Leakage
3.3 The Environment
3.4 The Adversary
3.5 The Full Interface
3.6 Executions
4 UC Emulation and Composition
4.1 Subsystem Replacement
4.2 Emulation and Absorption
4.3 Parallel Composition
4.4 Completeness of the Dummy Adversary
4.5 Concrete Security
5 Properties
6 Blockers
7 Relocation and Renaming
8 Concrete Costs
9 Responsive Calls
10 Core Language
11 Identical Until Bad
12 Sanitization
13 Randomness
13.1 Functionality
13.2 Properties
14 Storage
14.1 Functionality
14.2 Properties
15 Digital Signatures
15.1 Functionality
15.2 Properties
16 Public-Key Infrastructure
16.1 Functionality
16.2 Properties
17 Global Clock
17.1 Functionality
17.2 Properties
18 \(\Delta \)-Delayed Network
18.1 Functionality
18.2 Properties
19 \(\Delta \)-Delayed Authenticated Channel
19.1 Functionality
19.2 Properties
20 Realizing the Authenticated Channel
21 F_Sig: A Deeper Dive
21.1 Signature schemes and their games
21.2 The protocol \(\pi \)_Sig
21.3 The converse, and what properties cannot reach
21.4 A property of \(\pi \)_Sig that F_Sig lacks
Pending Issues
Pending Issues
Bibliography
Bibliography