Indistinguishability Obfuscation via Mathematical Proofs of Equivalence

Abstract

Over the last decade, indistinguishability obfuscation (iO) has emerged as a seemingly omnipotent primitive with numerous applications to cryptography and beyond. Moreover, recent breakthrough work has demonstrated that iO can be realized from well-founded assumptions. A thorn to all this remarkable progress is a limitation of all known constructions of general-purpose iO: the security reduction incurs a loss that is exponential in the input length of the function. This “input-length barrier” to iO stems from the non-falsifiability of the iO definition and is discussed in folklore as being possibly inherent. It has many negative consequences; notably, constructing iO for programs with inputs of unbounded length remains elusive due to this barrier. We present a new framework aimed towards overcoming the input-length barrier. Our approach relies on short mathematical proofs of functional equivalence of circuits (and Turing machines) to avoid the brute-force “input-by-input” check employed in prior works.– We show how to obfuscate circuits that have efficient proofs of equivalence in Propositional Logic with a security loss independent of input length.– Next, we show how to obfuscate Turing machines with unbounded length inputs, whose functional equivalence can be proven in Cook’s Theory PV.– Finally, we demonstrate applications of our results to succinct non-interactive arguments and witness encryption, and provide guidance on using our techniques for building new applications.To realize our approach, we depart from prior work and develop a new gate-by-gate obfuscation template that preserves the topology of the input circuit.

Topics & Concepts