Computationally Bounded Robust Compilation and Universally Composable Security

TL;DR

This paper lifts the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security, and provides a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security.

Abstract

Universal Composability (UC) is the gold standard for cryptographic security, but mechanizing proofs of UC is notoriously difficult. A recently-discovered connection between UC and Robust Compilation (RC)$\unicode{x2014}$a novel theory of secure compilation$\unicode{x2014}$provides a means to verify UC proofs using tools that mechanize equality results. Unfortunately, the existing methods apply only to perfect UC security, and real-world protocols relying on cryptography are only computationally secure. This paper addresses this gap by lifting the connection between UC and RC to the computational setting, extending techniques from the RC setting to apply to computational UC security. Moreover, it further generalizes the UC$\unicode{x2013}$RC connection beyond computational security to arbitrary equalities, providing a framework to subsume the existing perfect case, and to instantiate future theories with more complex notions of security. This connection allows the use of tools for proofs of computational indistinguishability to properly mechanize proofs of computational UC security. We demonstrate this power by using CryptoVerif to mechanize a proof that parts of the Wireguard protocol are computationally UC secure. Finally, all proofs of the framework itself are verified in Isabelle/HOL.

Figures (1)

• Figure 1: Visual depiction of the proofs of our main theorems. We prove solid black implications directly, derive dotted the orange implication as a special case, and conclude dashed purple results.

Theorems & Definitions (17)

• Definition 1: Perfect $\mathsf{UC}$ Emulation
• Definition 2: Indistinguishability Canetti-UC01
• Definition 3: Computational $\mathsf{UC}$ Emulation Canetti-UC01
• Definition 4: Robust Hyperproperty-Preserving Compiler
• Definition 5: Computational Indistinguishability of Programs
• Definition 6: Computationally-Robust Hyperproperty-Preservating Compiler
• Theorem 1: \ref{['cr:comprhc']} is Computational Preservation of $\mathit{CH}\xspace$
• Theorem 2: Computational $\mathsf{UC}$ and \ref{['cr:comprhc']} Coincide
• Definition 7: Predicate-Robust Hyperproperty-Preservating Compiler
• Proposition 1: \ref{['cr:predrhc']} expresses \ref{['cr:rhc']}