Computational-Bounded Robust Compilation and Universally Composable Security
summary
Proposes a precise equivalence showing that computationally robust hyper property preservation corresponds to computational UC emulation by adding polynomial-time restrictions and indistinguishability into the robust compilation framework, generalizing those predicates to arbitrary equivalences, and proving the math in Isabelle/HOL. Demonstrates the approach by mechanizing a UC-style proof of parts of WireGuard using CryptoVerif, and claims the framework subsumes perfect, statistical, and other security notions so mechanized tools can produce real computational UC proofs.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:04Universally Composable Security
- 2:50Robust compilation and UC
- 5:57Limitations of UC security
- 8:05Computationally bounded robust compilation
- 10:34Preserving hyperproperties
- 13:24Framework with predicates
- 16:35Summary and results
- 17:39Q&A
related talks
23mUniversal Composability is Robust Compilation
25mUniversal Composability is Secure Compilation
27mUniversally Composable Security for Program Partitioning
25mComposing Secure Compilers
08mShort Talk: Generalising secure compilation criteria
12mFully Abstract and Robust Compilation and How to Reconcile the Two, Abstractly
14mNon-interference Preserving Optimising Compilation
26mNon-Interference Preserving and Optimising Compilation with Hyperproperty Simulations