Indistinguishability Obfuscation via Mathematical Proofs of Equivalence
4Zhengzhong Jin (MIT)
https://simons.berkeley.edu/talks/zhengzhong-jin-mit-2023-03-21
Proof Complexity and Meta-Mathematics
Over the last decade, indistinguishability obfuscation iO has emerged as a seemingly omnipotent primitive in cryptography. 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.