Computationally Bounded Robust Compilation and Universally Composable Security
CoRR(2024)
摘要
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)x2014a novel
theory of secure compilationx2014provides 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
UCx2013RC 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要