In 1985, Goldwasser, Micali, and Rackoff introduced a compelling new notion of a proof, known as a proof of knowledge, in which a verifier interactively checks that a prover knows a satisfying witness for a claimed mathematical statement. For example, a verifier may check that a prover knows a witness solution for a prescribed Sudoku problem (and more generally any problem in NP). Interestingly, interaction affords seemingly paradoxical properties. For instance a prover can interactively demonstrate knowledge of a witness without revealing any information about it. Moreover, the demonstration itself can can be significantly shorter than the witness. For the past four decades, we have made significant progress in theoretical computer science by studying the time complexity, space complexity, and communication complexity of these interactions. Remarkably, we are also seeing proofs of knowledge being used in cryptographic applications to secure billions of dollars worth of assets.

Today, however, in search of practical efficiency, a growing body of work challenges the traditional paradigm by describing interactions in which the verifier does not fully resolve the prover's statement to true or false but rather reduces it to a simpler statement to be checked. Such interactive reductions, although central to modern proofs of knowledge, lack a unifying theoretical foundation. Towards a common language, we introduce reductions of knowledge, which reduce the task of checking knowledge of a witness in one relation to the task of checking knowledge of a witness in another (simpler) relation. We show that reductions of knowledge can be composed naturally, and thus serve as both a unifying abstraction and a theory of composition. As such, reductions of knowledge formalize a simple, but subtly powerful new perspective that proofs of knowledge are maps between propositions of knowledge.

We demonstrate that this is not merely a theoretical insight. In a very tangible sense, this perspective is becoming increasingly important for developing modern proofs of knowledge. We show that large swathes of the extant literature can be expressed crisply in our framework, as well as develop new techniques that cannot be expressed in preexisting models. Indeed, one of the early successes of our framework is the introduction of folding schemes, which are a particular type of two-to-one reduction of knowledge. We show that folding schemes have become an important tool for developing recursive proofs of knowledge, that is, proofs that demonstrate knowledge of other proofs. Recursive proofs have the potential to significantly scale decentralized computation due to their unique ability to handle stateful computation with dynamic control flow. As a result, recursive proofs (and the underlying folding schemes) have received significant recent interest in both industry and academia.

219 pages

Thesis Committee:
Bryan Parno (Chair)
Aayush Jain
Elaine Shi
Srinath Setty (Microsoft Research)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by reports@cs.cmu.edu