Keywords: proof complexity, zero-knowledge proofs.

Introduction↩︎

Ilango [1] defined a novel variant of zero-knowledge (ZK) proofs utilizing ideas coming from mathematical logic. The key idea in general terms is that the consistency of the existence of an object with a certain property may be just as useful as the existence itself. This is ubiquitous in logic (and found its way to proof complexity constructions too, cf. [2]). The construction of the new ZK, termed effectively ZK in [1], is conditional and rests upon two conjectures, one from cryptography and one form proof complexity, both discussed in Sec. 1.

The presentation in [1] avoids using even basic notions of mathematical logic (a theory, provability, consistency, etc.) and instead simulates them by various algorithms. In this note we embrace logic (the necessary background is briefly recalled in Sec. 1) and use it to give a reformulation of the new concept and a simple proof of the analogue of the main theorem of [1] (both in Sec. 2). A possibly interesting feature of our definition of a prover ZK relative to a theory is that the definition does not include the property of being indistinguishable from true (as does the definition of effectively ZK in [1]) but rather derives this property as a consequence of the definition.

In the proof of Theorem 2 we use model theory of arithmetic. The basic fact we use is a theorem of K.-Pudlák [3] that links the non-existence of short propositional proofs with the existence of extensions of models of bounded arithmetic. This is recalled in Sec. 1.

In Sec. 3 we offer a few proof complexity remarks and, in particular, we show that the concept of effectively ZK proofs (or ZK relative to a theory) can be transformed it into a genuinely zero-knowledge proofs, assuming a conjecture about the existence of a hard proof complexity generator (or assuming the existence of demi-bits) and allowing the parties to share a common random string.

The reader requiring more background on logic or proof complexity can find it in [4], [5].

1 Preliminaries↩︎

We are going to work with theories that can reason about computations and proofs, and we will follow to an extent the set-up in [3], [6]. A theory \(T\) is a set of sentences (axioms) in its language. It is convenient is to assume that

• \(T\) is a true theory in the language of bounded arithmetic \(S_2\) and contains its subtheory \(S^1_2\), and the property of being a \(T\)-axiom is p-time decidable.

Theories \(S_2\) and \(S^1_2\) are those introduced² by Buss [7] and their language extends the language of Peano arithmetic PA \(0,1, x\le y, x+y, x\cdot y\) by function symbols \(\lfloor \frac{x}{2}\rfloor\), \(|x| := \lceil \log(x+1)\rceil\) and \(x \# y := 2^{|x|\cdot|y|}\). The requirement on the language is not essential³.

To recall briefly some standard notation let us explain the meaning of the formula: \[\label{rfn} \forall z\;[Pr_T(\lceil E(\dot{z})\rceil ) \;\rightarrow\; E(z)]\;.\tag{1}\] Binary strings are identified with dyadic expansions of natural numbers and numbers are represented in the theory by closed terms, their dyadic numerals. The numeral for \(n\) is denoted \(\underline n\) and string \(w\) is represented in the theory by \(\lceil w\rceil := \underline n\), where \(n\) is the number identified with \(w\). We have that the lengths of \(w\), \(\lceil w\rceil\) and \(\log n\) are proportional to each other. The symbols in (1 ) mean the following: \(\dot{z}\) indicates that when substituting \(z := n\) we write \(\underline n\) and \(\lceil E(\dot{z})\rceil\) is then the term representing the formula \(E(\underline n)\), and \(Pr_T(x)\) is a natural formalization of the provability predicate for theory \(T\).

A theory \(T\) obeying (Th) can be considered⁴ as a propositional proof system (pps) in the sense of [8], a p-time function \(P\) whose range is exactly the set of propositional tautologies TAUT (strings in \(P^{(-1)})(\tau)\) are \(P\)-proofs of \(\tau\)). Following [6] define pps \(P(T)\) whose proofs of a tautology \(\tau\) are \(T\)-proofs of the sentence \(Taut(\lceil \tau\rceil)\), where \(Taut(x)\) is a natural formula defining TAUT, the set of propositional tautologies (cf. [6]).

A sequence of tautologies \(\Psi = \{\psi_n\}_n\) is p-time construable if there is a p-time function that computes \(\psi_n\) from \({1^{(n)}}\). The proof complexity assumption used in [1] is that for every pps \(P\) there a p-time construable sequence \(\Psi\) of tautologies that is hard for \(P\): for any \(c \geq 1\), all but finitely many \(\psi_n\) require \(P\)-proofs of size bigger than \(|\psi_n|^c\). This is equivalent to the non-existence of a pps that has only polynomial slow-down over any other pps for all but finitely many formula lengths. For this topic see [6] or the Optimality problem in [5]. Sequences of formulas \(\Psi\) used in [6] are propositional translations of the reflection principle for a pps.

We will work with models of \(T\). By (Th) \(\mathbf{N}\) is a model of \(T\) (the standard model) but \(T\) has also non-standard models \(\mathbf{M}\) with non-standard elements (those in \({\mathbf{M}}\setminus {\mathbf{N}}\)). Their use is quite convenient when dealing with asymptotic properties of natural numbers. In particular, all but finitely many natural numbers \(n \in {\mathbf{N}}\) have some definable property iff all nonstandard elements of any model \(\mathbf{M}\) of true arithmetic have the property (the overspill principle).

We will utilize the following theorem. It uses \(\Sigma^b_1\)-completeness that is provable in \(S^1-2\) (cf. [7] or [4]).

We also need to recall a notion entering the cryptographic assumption used in [1]. A non-interactive witness indistinguishability (NIWI) is a pair of deterministic p-time algorithms \(A, B\) with inputs and outputs:

• \(A : ({1^{(n)}}, \varphi, w, r) \rightarrow \pi\), where \(\varphi\) is a propositional formula and \(|\varphi| \le n\), \(w\) is an assignment to \(\varphi\) and \(r\) is a tuple of \(n^{O(1)}\) random bits,

• \(B : ({1^{(n)}}, \varphi, \pi) \rightarrow \{yes, no\}\)

that satisfy the following soundness and completeness conditions

1. If \(\varphi(w) = 1\) then \({ Prob}_r [B({1^{(n)}}, \varphi, A({1^{(n)}}, \varphi, w, r)) = yes]\;=\; 1\).

2. If \(\varphi \notin SAT\) then for all \(\pi\): \(B({1^{(n)}}, \varphi, \pi) = no\).

and also the following key indistinguishability condition. For any fixed \({1^{(n)}}, \varphi\) and varying \(w\) denote by \(D_w\) the distribution (whose support is the range of \(A({1^{(n)}}, \varphi, w, r)\)) induced by the algorithm \(A\) computing from random bits \(r\). Then it is required:

1. For every \(c \geq 1\) and \(n\) large enough if \(\varphi(w) = \varphi(w') = 1\) then \(D_w \approx_c D_{w'}\), where \(\approx_c\) denotes that no size \(\le n^c\) circuit distinguishes \(D_w\) from \(D_{w'}\) with advantage \(\geq n^{-c}\).

Note that the relations \(\approx_c\) (for fixed \(A,B\)) are properties of \({1^{(n)}}, \varphi, w, w'\) that are definable in the language of \(S_2\).

2 The prover↩︎

Given a NIWI \(A, B\) and a p-time sequence of tautologies \(\Psi = \{\psi_n(y)\}_n\) define, following Ilango [1], a prover for SAT as follows. A p-time algorithm \({Prover[A,B,\Psi]}\) receives

• input: \({1^{(n')}}\), propositional formula \(\varphi(x)\) s.t. \(|\varphi|\le n\), an assignment \(w = (u,v)\) to \(\varphi(x) \vee \neg \psi_n(y)\) and random bits \(r\),

and computes

• output: proof \(\pi := A({1^{(n')}}, \varphi \vee \neg \psi_n, w, r)\),

where \(n' :=|\varphi \vee \neg \psi_n|\). Verifier upon receiving \(\pi\) acts as \(B({1^{(n')}}, \varphi \vee \neg \psi_n, \pi)\). The soundness and the completeness of the NIWI imply that the prover is sound (using that \(\psi_n\) is not falsifiable) and complete too.

The ZK property is certified as in the classical case by a simulator; as there is no interaction the simulator just produces a proof (a distribution on proofs). But the usual requirements are weakened in three ways. First, the simulator is allowed to be a non-uniform⁵ probabilistic algorithm: the distribution on proofs is determined by a p-size circuit computing from random bits \(r\). The second weakening is technical in order to avoid talking about functions of super-polynomial growth: a simulator producing a distribution \(\approx_c\)-equivalent to the distribution produced by the prover is supposed to exists for all \(c \geq 1\) but not necessarily for all \(c\) at the same time. The last weakening is the key one: it is not required that a simulator (a circuit) actually exists but that its existence is consistent in the following sense.

The definition is different than that of effectively ZK in Ilango [1] but it aims at formalizing the same idea. However, a crucial difference is that it does not incorporate the requirement that the formula (?? ) is "indistinguishable from true", a property of statements defined in [1]. Our version of the property is the property established in Theorem 3.

Given a theory \(T\) obeying (Th) define a new theory \(T^*\) that extends \(T\) by a p-time set of new axioms: a stand alone axiom formalizing

• \(A, B\) is NIWI,

and then for each \(c,d \geq 1\) we add an instance of the reflection principle (1 ):

• \(\forall z\; [Pr_T(\lceil \neg \exists x (|x| \le (\dot{z})^d) \;Simulator_c(\dot{z}, x) \rceil ) \newline \;\rightarrow\; \neg \exists x (|x| \le (\dot{z})^d) \;Simulator_c(\dot{z}, x) ]\).

Let \({\mathbf{M}}\) be a non-standard model of the true arithmetic (and hence of \(T\) and \(T^*\)) and let \(m \in {\mathbf{M}}\) be any non-standard number. Let \({\mathbf{M}}_m \subseteq {\mathbf{M}}\) be the initial substructure with the universe \[\bigcup_{c \in {\mathbf{N}}} \{ u \in {\mathbf{M}}\;|\;|u| \le m^c \}\;.\] It is a model of \(S_2\) (in fact, of all true universal closures of bounded formulas). By the assumption that \(\Psi\) is hard for \(P(T^*)\) (and using the overspill) we get \[{\mathbf{M}}_m\;\models\;[P(T^*)\not\vdash \psi_m]\;.\] Theorem 1 thus yields an extension \({\mathbf{M}}^* \supseteq {\mathbf{M}}_m\) such that \[{\mathbf{M}}^*\;\models\;T^*\;+\;\neg \psi_m(v^*)=1\] for some \(v^* \in {\mathbf{M}}^*\).

Define in \({\mathbf{M}}^*\) circuit \(C_m\) that from \({1^{(m)}}, \varphi, r\) computes \[A({1^{(m')}}, \varphi \vee \neg \psi_m, w^*, r)\] where \(w^* := (0, v^*)\) and \(m' := |\varphi \vee \neg \psi_m|\).

Claim 1: For some \(d \in {\mathbf{N}}\) and all \(c \in {\mathbf{N}}\) it holds in \({\mathbf{M}}^*\) that \(C_m\) is a size \(\le m^d\) simulator for \({Prover[A,B,\Psi]}\) w.r.t. \(\approx_c\) and the length parameter \(m\).

To see this note that by the axiom of \(T^*\) that \(A,B\) is NIWI we have in \({\mathbf{M}}^*\) for all \(c \in {\mathbf{N}}\): \[D_w \;\approx_c\;D_{w^*}\] for all \(w := (u,0)\) such that \(\varphi(u)=1\).

Claim 2: For every \(c, e \in {\mathbf{N}}\): there is no size \(\le m^e\) \(T\)-proof in \({\mathbf{M}}\) of \[\label{fla} \neg \exists x (|x| \le {\underline m}^d) \;Simulator_c(\underline m, x)\;.\qquad{(2)}\]

This is because such a proof would be in \({\mathbf{M}}^*\) too and by the second extra axiom of \(T^*\) the sentence (?? ) would be true, contradicting Claim 1.

The parameter \(m\) was chosen at the beginning to be an arbitrary non-standard number and thus the overspill in \({\mathbf{M}}\) implies that for all \(c, e \in {\mathbf{N}}\), for all but finitely many \(n \in {\mathbf{N}}\) there is no size \(\le n^e\) \(T\)-proof of \[\neg \exists x (|x| \le {\underline n}^d) \;Simulator_c(\underline n, x)\;.\] Hence \({Prover[A,B,\Psi]}\) is ZK relative to \(T\).

For the next statement we shall consider (following [6]) formulas \(S(y)\) of the form \[\label{sfla} \forall u_1 (|u_1| \le y) \dots \forall u_k (|u_k| \le y) Q_1 v_1 \le y \dots Q_\ell v_\ell \le y\;S_0(y, \overline{u}, \overline{v})\tag{2}\] where \(S_0\) is open. The formula is not bounded but a statement analogous to the \(\Sigma^b_1\)-completeness in bounded arithmetic holds (cf. [4], [6].

The property in the following theorem corresponds to the property of being indistinguishable from true of [1] where it is a part of the definition of effectively ZK proofs.

Take \(d \geq 1\) provided by Definition 1, \(n\) large enough and assume (?? ) has a size \(\le n^e\) \(T\)-proof. Assuming \(S(n)\) is false, sentence \(\neg S(\underline n)\) has a size \(\le n^a\) \(T\)-proof by Lemma 1. Combining the two \(T\)-proofs yields a \(T\)-proof of \[\neg \exists x (|x| \le {\underline n}^{d}) \;Simulator_c(\underline n, x)\] of size \(\le n^{e'}\) for fixed \(e'\) and \(n\) large enough. That contradicts Definition 1.

3 Proof complexity remarks↩︎

The soundness of \({Prover[A,B,\Psi]}\) rests upon the fact that all formulas in \(\Psi\) are tautologies. However, theory \(T\) (representing the verifier) cannot prove this fact as otherwise \(\Psi\) would not be hard for \(P(T)\) even. Hence the verifier is left to trust that \({Prover[A,B,\Psi]}\) is sound. If we assume, as seems prudent to do, that the prover has same strength as the verifier (i.e. corresponds to \(T\) as well) then it needs to trust the soundness as well. In other words, both the prover and the verifier are handed down \(\Psi\) to use and they cannot verify that the resulting algorithm is sound. Moreover, in order to built a simulator, the verifier needs to know the algorithm the prover uses to compute the sequence \(\Psi\). Then the first thing the verifier could do is to add to the base theory \(T\) as a new axiom \(\forall x\;Taut(\psi_{x})\), and this causes that \({Prover[A,B,\Psi]}\) stops being ZK for (the upgraded) \(T\).

Even if the reader is inclined to ignore these issues there still remains the fundamental question how to construct \(\Psi\) hard for a given specific proof system \(P\) or, equivalently by [6], how to construct a proof system \(Q(P)\) that is not simulated by \(P\) (not even on infinitely many formula lengths). There are several conjectural constructions of \(\Psi\) but we do not have a proof that one of them works even assuming that a hard sequence for \(P\) exists. For various ways of thinking about this fundamental problem the reader may consult the original [6], more recent K. [10], Khaniki [11] or Pudlák [12] or [5]

One can bypass these problems by using instead of \(\Psi\) hard formulas determined by proof complexity generators. This was pointed out already by Ilango [13]. It lead him to consider non-uniform provers and verifiers. However, it is possible to get uniform probabilistic prover and verifier if one allows them to share a random string. The resulting ZK is then ZK in the usual sense. We shall now outline a construction based on [14].

By a generator we mean any map \(g\) with the property that the range of its restriction \(g_n\) to \({\{0,1\}^n}\) is a subset of \({\{0,1\}^m}\) where \(m = m(n) > n\), and \(g_n\) is computed by a circuit \(C_n\) of size \(m^{O(1)}\). The \(\tau\)-formula \(\tau(g)_b\) for \(b \in {\{0,1\}^m}\) is a canonically defined formula expressing that \(b \notin Rng(C_n)\); it is a tautology iff \(b\) is outside of the range of \(g_n\). Generator \(g\) is hard for a pps \(P\) if for all \(e \geq 1\), all but finitely many tautologies \(\tau(g)_b\) require a \(P\)-proof of size bigger than \(|\tau(g)_b|^e = m^{O(e)}\). A central conjecture of the theory states that there is a generator that is hard for all pps and, in fact, that it can be found uniform p-time with \(m = n+1\). An exposition of the theory can be found in [2].

Ilango [13] and Ren et al. [15] proved, under slightly differently formulated assumption about the existence of demi-bits of super-polynomial hardness, that such a \({\cal P}/poly\) generator hard for any specific pps exists. Ilango [13] then used an additional argument to show that there is one \({\cal P}/poly\) \(g\) hard for all pps. Demi-bits were defined by Rudich [16]: it is a p-time generator \(G\) with \(m = n+1\) such that no subexponential size non-deterministic circuit can define a sub-exponential part of the complement of the range of \(G\).

We will now refer to the construction of a proof complexity generator \(g_s\) from \(G\) as given in the proof of [14]. That construction uses both [13], [15] but it simplifies it using a result from [9]. That allows to prove the claim stated below.

We follow closely the proof of [14], changing only slightly the parameter \(m\). Start with a p-time demi-bit \(G : {\{0,1\}^n}\rightarrow {\{0,1\}^m}\) where \(m = 2n\) (in [14] we use \(m = {{n+\lceil\log n\rceil + 1}}\) to have a weaker assumption on the stretch of demi-bits). Then any \(m^2\) bits \(s\) determine a map \(g_s : \{0,1\}^{n + \log m} \rightarrow {\{0,1\}^m}\) that is computed in deterministic p-time with \(s\) as an advice. The construction has the following property:

Claim: For a random string \(s\) the map \(g_s\) is hard for all pps with the probability at least \(1 - 2^{-n^{\Omega(1)}}\).

If the prover and the verifier share a random string \((s,s') \in \{0,1\}^{m^2}\times {\{0,1\}^m}\) they can use \(s\) to define \(g_s\) and \(s'\) to pick a random \(b \in {\{0,1\}^m}\) (which is outside of the range of \(g_s\) with the probability exponentially close to \(1\)), and use \(\tau(g_s)_{b}\) instead of \(\psi_n\) in the ZK proofs.

A potential way how \(g_s\) could be replaced by a uniform generator \(g\) is discussed in [14]. However, note that even with uniform \(g\) the parties would still need a common random string \(s'\) to choose \(b\).

References↩︎