UC for Gamers

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 Δ-Delayed Network
18.1 Functionality
18.2 Properties
19 Δ-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 π_Sig
21.3 The converse, and what properties cannot reach
21.4 A property of π_Sig that F_Sig lacks
Pending Issues
Bibliography

¹A good value exists whenever the space \(\Clean \) draws from is infinite and everything it excludes beyond non-membership is a value named in the context \(c\). Both halves are needed for the predicates of Chapter 15: membership in an infinite \(\Keys \) or \(\Sigs \) is the first conjunct of each, and everything else they exclude is an entry of a table passed in \(c\). Under Definition 4.30 the context is finitely supported in any execution — a bounded run records finitely many entries — so the excluded set is finite inside an infinite space.