UC for Gamers

Available format(s): HTML | PDF | LaTeX source

The HTML edition is generated from the same LaTeX as the PDF by scripts/build_uc_html.sh, split one page per chapter and per section, with the full table of contents in a sidebar on every page. Its mathematics is text rather than images, so it is searchable and selectable, and its interface boxes carry the same computed line numbers the printed book uses. The PDF remains the reference, since the HTML’s page breaks and floats are not the printed ones.

Abstract

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, this book sets 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.

Contents

Each entry opens that chapter in the HTML edition, which carries the sections under it in its sidebar.

Notebook

A NotebookLM notebook for this book, for putting questions to it directly. It opens behind a Google sign-in: the link redirects to an account page for anyone not already signed in.