Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
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.
