• 作者:Maksym Petkus
  • 翻译 & 注解:even@安比实验室(even@secbit.io)
  • 校对:valuka@安比实验室
  • 本系列文章已获作者中文翻译授权
  • 翻译原链接

约束和公共输入 Constraints and Public Inputs

约束 Constraints

我们的分析主要集中在运算的概念上。但是,协议实际上不是去做”计算“,而是检验输出值是否是操作数正确运算得到的结果。所以我们称之为约束,即一个 约束 去为预定义的“程序”提供有效值,而无论这个“程序”是什么。多个约束组成的系统被称为“约束系统”(在我们的例子中这是一个一阶约束系统,或被称为 R1CS

@Maksym(作者):这里其实隐含了寻找所有正确答案的一个方法就是对所有可能的组合值进行一次暴力破解,然后只选择一个满足的约束,或者使用可满足约束的更精密的技术 con18 even@安比实验室:请注意这个约束是定义在算术电路,或者布尔电路上。因为这两类电路的可满足性问题是 NP-Complete 问题。

因而我们也可以使用约束来确保其它的关系。例如,如果我们想要确认变量 的值只能为 0 或 1(即二进制数),我们可以用一个简单的约束去做这件事: 我们也可以约束 的值只能为 2: 一个更复杂的例子是确保数字 是一个 4-bit 的数字(也称为半字节 nibble),换句话说可以用 4 个bit 来表示出 , 我们也可以称这个为“确保取值范围” , 因为一个 4-bit 的数字可以代表 的组合,因而也就是从 0 ~ 15 范围内的 16 个数字。如

Therefore if is a 4-bit number, then ,for some boolean ,  The constraint can be following: 并且为了确保 都是二进制数我们需要增加约束: 可以写成 Circom 代码:

#![allow(unused)]
fn main() {
a * 1 = 8*b3 + 4*b2 + 2*b1 + 1*b0
b0 * b0 = b0
b1 * b1 = b1
b2 * b2 = b2
b3 * b3 = b3
}

更复杂的约束也可以用这种方式表示,以此来确保使用的值满足规则。需要注意的是,上述约束 在当前操作的构造中是不可能的: 因为值 1 (以及前面约束中的 2)必须通过 表达出来,其中 c 可以被固定到 proving key 中,但是因为 v 是由 提供的,所以可以是任何别的值。尽管我们可以通过设置 c = 0 来强制 变成 0,但是在我们前面受限的构造方法中很难找到一个约束来强制 为 1。于是, 需要有一种办法来设置 的值

首先,我们需要明确 这个特殊变量的角色。在 zk-SNARK的 约束系统中,它是被预设为 1 的。换句话说,无论其他变量如何变化, 的值始终应该是1。

然后,该部分内容提到的 ,实际上是约束系统中的一个公式,其中 是证明者在证明过程中需要选择的一个值, 是我们前面说的那个始终为 1 的特殊变量。

然后,它提到,即使我们可以通过设置 来使得 为0,但在当前的构造方法中,我们却无法找到一个约束来强制 为 1 。这个意思是说,在我们的构造方法中,我们可以通过选择不同的 使得 为任何我们希望的值,但这并不能保证 始终为1

even@安比实验室: 我们前文中提到的表达式的约束关系就称为 R1CS

Public Inputs and One (公共输入和 1)

如果不能根据 的输入对其进行检查,例如,知道证明者已将两个值相乘而不知道结果和/或值是什么,那么证明的可用性将受到限制。虽然可以在 proving key 中通过“硬编码(hardwire)”来进行验证一些特定的值(如,约束某步乘法运算的结果必须为 12 ),但这就需要针对每一个所需的的 “verifier 输入”生成单独的密钥对 (this would require to generate separate pair of keys for each desired “verifier’s input.”)

even@安比实验室: 这样会严重限制实用性,电路需要支持参数。

因而如果可以由 为计算指定一些值(输入/输出),包括 ,而不是由 来控制, 那证明就可以变得更通用!! (Therefore it would be universal if the verifier could specify some of the values (inputs or/and outputs) for the computation, including the  , instead of the .)

首先,我们看一下要证明的值 Because we are using the homomorphic encryption it is possible to augment these values, for example, we can add another encrypted polynomial evaluation (利用同态加密,我们可以扩大这些值) which means that the verifier could add other variable polynomials to the already provided ones. Therefore if we could exclude necessary variable polynomials from the ones available to the prover, the verifier would be able to set his values on those variables, while the computation check should still match. 这意味着验证者 可以将 other variable polynomials 添加到已经提供的 polys 中。因此,如果我们可以从提供给 的变量多项式中, 排除(exclude) necessary variable polys, 验证者 将能够在这些变量上设置他的值,而计算检查应该仍然匹配。

也就是说, 这样如果我们能够在提供给 的变量多项式中排除必要的一项, 就可以在这一项变量多项式上设置他自己的值,并且使得检查依然能够通过

It is easy to achieve since the is already constraining the prover in the choice of polynomials he can use empolying the α-shift. Therefore those variable polynomials can be moved from the proving key to the verification key while eliminating its α-s and β checksum counterparts. 这很容易实现,因为 已经限制了 选择他可以使用 α-shift 的多项式。因此,这些可变多项式可以从 proving key 转移到 verification key ,同时消除其 α-s 和 β 校验和对应项。

也就是说, 因为 早已能通过加入 α-shift 来限制 选择多项式,所以这个应该很容易实现。因而当消除了它的 校验和对应的项,这些可变多项式就可以从 proving key 转移到 verification key 当中去了

必要的协议更新为:

Setup (需自行对比 former protocol version)

  • …将 个 variable polys 全部分为两组:
    • 项: , 对 也做同样的计算。这里对于索引 0 保留值 (where idx-0 is reserved for the value of )
    • 项:
    • … 对 也做同样的计算
  • 设置 proving key
  • 添加到 verification key

Proving :

  • …为 的多项式计算 , 其中 , and similarly for

  • Provide the Proof : Verification :

  • 的变量多项式赋值,并加 (and add to 1) : 做同样的计算 关于为啥要 +1 : 需要一种机制,让 能够控制一些变量的值,而不是由 控制, 通过同态加密, 让v_one 就是一个始终为 1 的特殊变量 (先感性理解下吧 …)

  • 变量多项式约束检查: 做同样的计算

变量值一致性检查:

有效计算检查:

注意:根据协议(单个变量操作数多项式 的章节)的性质,由多项式 表示的值 已在相应的运算中具备了合适的值,因此不需要再赋值了

注意: 将不得不在验证步骤中做额外的工作,使得赋值的变量成比例。

这实际上是把一些变量从 手中拿到 的手中,并同时保持等式相等。 因而只有当 的输入中使用相同值的时候, 有效计算检查 才依然成立。

1 这个值相当重要,它能够通过与任意一个常数项相乘来生成这个值(从选择的有限域上),例如,用 123 去乘以 a

even@安比实验室: 这里将原本由 赋值的一些变量改为由拿到 赋值,使得 不得不与 保持相同的输入。这不仅解决了 参数输入的问题,也间接解决了常数赋值的问题

Zero-Knowledge Computation

Zero-Knowledge Proof of Computation

(计算的零知识证明) 自从引入通用计算协议(计算的证明这一章节),我们一直放弃了 零知识 的性质,这是为了让协议的改进变得更简单。至此,我们已经构建了可验证的计算协议。

以前我们使用随机数 δ-转换来构造多项式的“零知识” 证明,这种方法能够使得证明与随机数无法区分(零知识这一章节): 通过计算我们证明了: 尽管我们可以通过用相同 δ × 多项式的方法来调整解决方案,即提供随机值 ,这依然能够通过 有效计算检查 来满足配对验证: 但是问题是使用相同的 会妨碍安全性,因为我们在证明中分别用了以下这些值:

  • 其他人可以很容易得辨认出两个不同的多项式值是否相同,以此来获取一些知识,即:
  • 的不同值之间潜在的微小关系可能会通过暴力破解来区分开来,例如如果 ,就可以对 取值反复校验 ,只需要执行 5 步就可以揭示出两者 5 倍区别的关系。同样的暴力破解也可以用在破解加密值的加法运算上,如:
  • 证明元素之间的其它关系也可能会被发现,例如,如果 ,那么也就表示

注意:一致性检查优化 使得挖掘数据关系变得更加困难了,但是依然能够发现一些关系 ,且不说 可以选择特定 来为揭示知识提供便利(只要这不是一个多样化的

最终,我们需要对每一个多项式的值使用不同的随机数 ,例如: 为了解决等式右边不相等的问题,我们不必改变协议,只要修改证明的值 即可。 这里 Delta ( ) 代表为了平衡方程另一侧的随机性而对 做的处理,?⃝ 代表 乘法运算或者 加法运算(这个反过来也适应了除法和减法)。

  • 如果我们选择用乘法 (?⃝ = ×) 来计算 ,也就意味着不太可能有较大的概率可以找到一个 ,因为存在随机性: 设置 ,于是就变成了: 但是如前文所述,这个妨碍了零知识的性质,更重要的是这个结构也不再适合 verifier 的输入多项式,因为它们必须是 相应的倍数,这就需要额外的交互了

我们可以尝试把随机数加到变量上:

但是随机数是不可除尽的。尽管我们可以用 去乘以每一个 ,但由于我们已经用了 乘以 是组成加密结果的一部分(即 相等),因此在没有使用配对(它的结果在另一个数值空间内)的情况下是不能计算出 的。同样也不能使用 的幂(from to )的加密值对 进行加密计算, 的阶将达到 并且,基于上述同样的原因也无法计算这个随机操作数多项式的值: 于是我们应该用加法(?⃝ = +)来使用 ,因为它可以同态地计算。

分子中的每一项都是 的倍数,因而我们可以将其与 相乘使它可以被分母整除:

这样就可以在加密的空间中进行“有效计算检查”了: 于是既隐藏了加密值,又使得等式可以通过 有效计算 的检查 这个结构就是统计学上的零知识 因为增加了 的均匀随机倍数(参见 [Gen+12] 中的定理 13)

注意:这种方法和 的操作数也是一致的,即:

因而当且仅当 使用了 的值来构造证明(即, ,这个有效计算的检查依然是成立的,更多的细节看下一部分

为了使得 “变量多项式限制” 和 “变量值一致性”检查与 零知识 的修改一致,就有必要去增加以下的参数到 proving key 中: 非常奇怪的是最初的 Pinocchio 协议[Par+13]主要关注可验证的计算,而较少涉及 零知识 性质,这其实只需要一点点小修改,这个几乎是没有什么成本的。

even@安比实验室: 与前文中的零知方案不同,这里通过相加而不是相乘的方式来确保 prover 知识的零知性。

Pinocchio 协议是针对 GGPR 论文的改进,在3.1节中也提到了实现零知识只需要沿用 GGPR 论文的方法即可,并不是这篇论文的贡献。另外,Pinocchio 协议论文侧重工程实践,在2013年时,零知识证明还并没有得到应用。真正的应用还是自从 ZCash 起始

zk-SNARK 协议

在这一步步的改进之后,我们得到了最终版本的 zkSNARK,又名 Pinocchio [Par + 13],协议 (zero knowledge is Optional, 并用紫色标注出来了),就是:

Setup

  • 选择生成元 和加密配对

  • 将变量总数为 , 其中输入/输出变量数位 的函数 ,转换为阶数为 大小为 的多项式形式(QAP)

  • 选择随机数

  • 设置 和操作数生成元

  • 设置 proving key

  • 设置 verfication key

Proving

  • 代入输入值 ,执行 计算获取所有的中间变量值
  • 把所有未加密的变量多项式赋值给 ,并对 做同样的计算
  • 选择随机数
  • 计算
  • 将 prover 的变量值赋值给加密的可变多项式
  • 再用同样的方式计算
  • 为变量值一致性多项式赋值 :
  • 计算证明

Verification

  • 解析提供的证明为

  • 输入/输出 赋值给 verifier 的加密多项式并加 1 : 并对 做同样的计算

  • 可变多项式约束检查: 并对 做同样的检查

  • 变量值一致性检查:

  • 有效的计算检查:

结论

我们最终完成了一个允许证明计算的有效协议:

  • 简明 (Succinctly) —— 独立于计算量,证明是恒定的,小尺寸的
  • 非交互性 (Non-interactive) —— 证明只要一经计算就可以在不直接与 prover 交互的前提下使任意数量的 verifier 确信
  • 可论证的知识 (with Argument of Knowledge) —— 对于陈述是正确的这点有不可忽略的概率,即无法构造假证据;并且 prover 知道正确陈述的对应值(即:证据),例如,如果陈述是 “B 是 sha256(a) 的结果” 那么就说明 prover 知道一些值 a 能够使得 B = sha256(a) 成立,因为 B 只能够通过 a 的知识计算出来,换句话说就是无法通过 B 来反算出 a(假定 a 的熵足够)。
  • 陈述有不可忽略的概率是正确的 (even@安比实验室: 这里指 Soundness 可靠性),即,构造假证据是不可行的
  • 零知识 ( zero-knowledge) —— 很“难”从证明中提取任何知识,即,它与随机数无法区分。

even@安比实验室: 所谓 Argument——论证,区别于 Proof —— 证明。 Pinocchio 协议是 Argument 而非 Proof。这是因为 Pinocchio 的可靠性是 Computational Soundness,Statistical ZK,这一类的证明系统被称为 Argument。所谓的 Computational Soundness 暗含了这样的事实:如果 Prover 计算能力足够强大的话,可以破坏可靠性。

基于多项式的特殊性质,模运算,同态加密,椭圆曲线密码学,加密配对和发明者的聪明才智才使得这个协议得以实现。

这个协议证明了一个特殊有限执行机制的计算,即在一次运算中可以将几乎任意数量的变量加在一起但是只能执行一次乘法,因而就有机会优化程序以有效地利用这种特性的同时也使用这个结构最大限度地减少计算次数。

为了验证一个证明, verifier 并不需要知道所有的秘密数据,这一点很关键,这就使得任何人都可以以非交互式方式发布和使用正确构造的 verification key。这一点与只能让一个参与者确信证明的“指定 verifier”方案相反,因而它的信任是不可转移的。在 zkSNARK 中,如果不可信或由单方生成密钥对,则可以实现这个属性。

零知识证明构造领域正在不断发展,包括引入了优化([BCTV13, Gro16, GM17]),改进例如可更新的 proving keyverification key([Gro+18]),以及新的构造方法(Bulletproofs [Bün+17], ZK-STARK [Ben+18], Sonic [Mal+19])