Indistinguishability Obfuscation via Mathematical Proofs of Equivalence

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 "inputlength 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 P V . -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.