Computational-Bounded Robust Compilation and Universally Composable Security

Explore the connection between Universal Composability (UC) and Robust Compilation (RC) in cryptographic security through this conference talk. Delve into the extension of the UC-RC connection to computational settings, enabling the mechanization of computational UC security proofs. Learn how this framework generalizes beyond computational security to encompass arbitrary equalities, providing a versatile approach for various security theories. Discover the practical application of these concepts through a mechanized proof of computational UC security for parts of the Wireguard protocol using CryptoVerif. Gain insights into the verification process of the framework itself using Isabelle/HOL, demonstrating the power of formal methods in cryptographic security analysis.