Symbolic security of garbled circuits

Baiyu Li; Daniele Micciancio

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

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

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Published elsewhere. Minor revision. IEEE CSF 2018
DOI: 10.1109/CSF.2018.00018
Keywords: symbolic cryptography garbled circuit formal methods in cryptography computational soundness symbolic analysis
Contact author(s): baiyu @ cs ucsd edu
History: 2019-10-04: last of 3 revisions; 2018-02-07: received; See all versions
Short URL: https://ia.cr/2018/141
License: CC BY

BibTeX

@misc{cryptoeprint:2018/141,
      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},
      url = {https://eprint.iacr.org/2018/141}
}