第3章 零知识证明
零知识证明技术是现代密码学三大基础之一,由格沃斯(S.Goldwasser)、米加里(S.Micali)及拉科夫(C.Rackoff)在20世纪80年代初提出(SHAFI GOLDWASSER, SILVIO MICALI,AND CHARLES RACKOFF, 1989.《The Knowledge Complexity of Interactive Proof System》,下载地址:http://crypto.cs.mcgill.ca/~crepeau/COMP647/2007/TOPIC01/GMR89.pdf)。
早期的零知识证明由于其效率和可用性等限制,未得到很好的利用,仅停留在理论层面。
从2010年开始,零知识证明的理论研究才开始不断突破,同时区块链也为零知识证明创造了大展拳脚的机会,使之走进了大众视野。
零知识证明的英文全称是zero-knowledge proofs,简写为ZKP,是一种有用的密码学方法。
证明过程涉及两个对象:一个是宣称某一命题为真的示证者(prover),另一个是确认该命题确实为真的验证者(verifier)。
所谓“零知识”,意味着当证明完成后,验证者除了获得对命题正确与否的答案之外,其他信息一无所知,获得的“知识”为零。
零知识证明是构建信任的重要技术,也是区块链这个有机体中不可缺少的一环。
什么是证明?
最早接触“证明”这个概念,应该是在中学课程中见到的各种相似三角形的证明。当我们画出一条“神奇”的辅助线之后,证明过程突然变得简单。其实,证明的发展经历了漫长时间长河的沉淀。
1.古希腊时期:证明=知其然,更知其所以然
数学证明最早源于古希腊。古希腊人发明了公理与逻辑,他们用证明来说服对方,而不是靠权威。这是彻头彻尾的“去中心化”。自古希腊以来,这种方法论影响了整个人类文明的进程。
2.20世纪初:证明=符号推理
到了19世纪末,康托、布尔、弗雷格、希尔伯特、罗素、布劳威、哥德尔等人定义了形式化逻辑的符号系统。而“证明”则是利用形式化逻辑的符号语言编写的推理过程。逻辑本身靠谱么?逻辑本身“自洽”吗?逻辑推理本身对不对,能够证明吗?这让数学家/逻辑学家/计算机科学家发明了符号系统。
3.20世纪60年代:证明=程序
又过了半个世纪,到20世纪60年代,逻辑学家哈斯卡·咖里(Haskell Curry)和威廉·霍华德(William Howard)相继发现了在“逻辑系统”和“计算系统——Lambda演算”中出现了很多“神奇的对应”,这就是后来被命名的“柯里-霍华德对应”(Curry-Howard Correspondence)。这个发现使得大家恍然大悟,“编写程序”和“编写证明”实际上在概念上是完全统一的。
在这之后的50年,相关理论与技术的发展使得证明不再停留在草稿纸上,而是可以用程序来表达。这个同构映射非常有趣:程序的类型对应于证明的定理,循环对应于归纳,在直觉主义框架中,证明就意味着构造算法,构造算法实际上就是在写代码。(反过来也成立)
目前,在计算机科学领域,许多理论的证明已经从纸上的草图变成了代码的形式,比较流行的“证明编程语言”有Coq、Isabelle、Agda等。采用编程的方式来构造证明,证明的正确性检查可以机械地由程序完成,并且许多重复性的劳动可以由程序来辅助完成。数学理论证明的大厦正在像计算机软件一样逐步地构建。1996年12月,麦昆(W.McCune)利用自动定理证明工具EQP证明了一个有63年历史的数学猜想“Ronbins猜想”,《纽约时报》随后发表了一篇题为Computer Math Proof Shows Reasoning Power的文章,再一次探讨机器能否代替人类产生创造性思维的可能性。
利用机器的辅助确实能够有效地帮助数学家的思维抵达更多未知的空间,但是“寻找证明”仍然是最有挑战性的工作。“验证证明”则必须是一个简单、机械并且有限的工作。这是一种天然的“不对称性”。
4.20世纪80年代:证明=交互
时间拨到1985年,乔布斯刚刚离开苹果,而格沃斯(S. Goldwasser)博士毕业后来到了MIT,与米加里(S.Micali)、拉科夫(Rackoff)合写了一篇能载入计算机科学史册的经典:《交互式证明系统中的知识复杂性》。
他们对“证明”一词进行了重新的诠释,并提出了交互式证明系统的概念:通过构造两个图灵机进行“交互”而不是“推理”,来证明一个命题在概率上是否成立。“证明”这个概念再一次被拓展。
交互证明的表现形式是两个(或者多个)图灵机的“对话脚本”,或者称为Transcript。而这个对话过程中有一个显式的“证明者”角色,还有一个显式的“验证者”角色。其中,证明者向验证者证明一个命题成立,同时还“不泄露其他任何知识”。这种证明方式就被称为“零知识证明”。
证明凝结了“知识”,但是证明过程却可以不泄露“知识“,同时这个证明的验证过程仍然保持简单、机械,以及有限。