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.

翻译：泛组合安全（UC）是密码学安全的黄金标准，但机械化证明UC的难度众所周知。近期发现的UC与鲁棒编译（RC）——一种新颖的安全编译理论——之间的关联，为利用机械化等式结果验证UC证明提供了新途径。然而，现有方法仅适用于完美UC安全，而依赖密码学的现实协议仅具备计算安全性。本文通过将UC与RC的关联提升至计算设定，填补了这一空白，并将RC领域的技术扩展至计算UC安全。此外，该工作进一步将UC-RC关联从计算安全性推广至任意等式，构建了一个既涵盖现有完美情形、又能实例化未来更复杂安全概念的理论框架。这一关联使得计算不可区分性证明工具可用于恰当地机械化计算UC安全证明。我们通过使用CryptoVerif机械化证明Wireguard协议部分组件具备计算UC安全性，展示了这一能力。最后，框架本身的所有证明均在Isabelle/HOL中经过验证。