Symbolic security of garbled circuits

Authors: Baiyu Li and Daniele Micciancio

Paper Information

Title:Symbolic security of garbled circuits
Authors:Baiyu Li and Daniele Micciancio
Proceedings:CSF CSF Proceedings
Editors: Stephen Chong, Stephanie Delaune and Deepak Garg
Keywords:symbolic cryptography, symbolic security, garbled circuit, formal methods for security, computational soundness, greatest fixed point

ABSTRACT. We present the first computationally sound symbolic analysis of Yao's garbled circuit construction for secure two party computation. Our results include an extension of the symbolic language for cryptographic expressions from previous work on computationally sound symbolic analysis, and a soundness theorem for this extended language. We then demonstrate how the extended language can be used to formally specify not only the garbled circuit construction, but also the formal (symbolic) simulator required by the definition of security. The correctness of the simulation is proved in a purely syntactical way, within the symbolic model of cryptography, and then translated into a concrete computational indistinguishability statement via our general computational soundness theorem. We also implement our symbolic security framework and the garbling scheme in Haskell, and our experiment shows that the symbolic analysis performs well and can be done within several seconds even for large circuits that are useful for real world application.

Talk:Jul 10 12:00 (Session 54A: Secure computation)