Cryptology ePrint Archive: Report 2018/141

Symbolic security of garbled circuits

Baiyu Li and Daniele Micciancio

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 applications.

Category / Keywords: foundations / symbolic cryptography, garbled circuit, formal methods in cryptography, computational soundness, symbolic analysis

Original Publication (with minor differences): IEEE CSF 2018

Date: received 6 Feb 2018, last revised 4 Oct 2019

Contact author: baiyu at cs ucsd edu

Available format(s): PDF | BibTeX Citation

Note: Defined definitions and added more references. Also added a symbolic analysis of Yao's computational secret sharing scheme in the appendix.

Version: 20191004:191150 (All versions of this report)

Short URL:

[ Cryptology ePrint archive ]