Paper 2018/141

Symbolic security of garbled circuits

Baiyu Li and Daniele Micciancio


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.

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

Available format(s)
Publication info
Published elsewhere. Minor revision. IEEE CSF 2018
symbolic cryptographygarbled circuitformal methods in cryptographycomputational soundnesssymbolic analysis
Contact author(s)
baiyu @ cs ucsd edu
2019-10-04: last of 3 revisions
2018-02-07: received
See all versions
Short URL
Creative Commons Attribution


      author = {Baiyu Li and Daniele Micciancio},
      title = {Symbolic security of garbled circuits},
      howpublished = {Cryptology ePrint Archive, Paper 2018/141},
      year = {2018},
      doi = {10.1109/CSF.2018.00018},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.