Universal Composability is Robust Compilation
summary
Paper claims UC security and robust compilation are equivalent under clear axioms and gives a recipe to mechanize UC proofs. It axiomatizes UC semantics, maps protocols↔programs, and uses back-translation proof techniques plus a ported dummy attacker theorem to build simulators. Implementation with DeepSEaC yields the first mechanized UC proof of one-bit commitment in the adaptive-corruption setting after dropping hiding and adding a few lines to encode the security argument.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:52UC challenges and goals
- 3:36UC key concepts
- 7:10Robust compilation background
- 10:02UC versus robust compilation
- 13:11UC compilation benefits
- 15:18Mechanizing UC proofs with DeepSec
- 18:06Paper contributions
- 19:09Summary
- 19:30Q&A
related talks
25mUniversal Composability is Secure Compilation
22mComputational-Bounded Robust Compilation and Universally Composable Security
27mUniversally Composable Security for Program Partitioning
25mComposing Secure Compilers
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
15mMy Journey in Secure Compilation
08mShort Talk: Generalising secure compilation criteria
31mSequential Composition of Rational Proofs