著者：郭優
この記事は Github に更新されました。https://github.com/
導入：
ブロックチェーンは決して「技術」ではないと思います。それはむしろフィールドのようなもので、すべてを包括します。形而上学的に言えば、ブロックチェーンはさまざまな理論技術を統合した有機体に似ています。
ゼロ知識証明は信頼を構築するための重要なテクノロジーであり、ブロックチェーンという組織の不可欠な部分です。
ゼロ知識証明は、オンチェーン データとオフチェーン コンピューティングを接続するための重要なテクノロジーであり、オンチェーン データのプライバシー保護を実現する重要な方法でもあります。
証明する
"証明する"今昔
証拠とは何ですか？私と同じような人も多いのではないでしょうか この二つの単語を見ると、中学受験の三角形に似たさまざまな幾何学図形が頭に浮かびます 先生が魔法のように補助線を引くと、証明の過程が突然見えてきます、そしてなぜ期待していなかったのかを後悔します。
古代ギリシャ語: 「証拠」 == 「洞察力」
数学的証明は古代ギリシャに始まりました。彼らは公理や論理を発明（発見）し、権威ではなく証明によってお互いを説得しました。これは徹底的な「分散化」です。古代ギリシャ以来、この方法論は人類の文明の全過程に影響を与えてきました。
上の写真は「ピタゴラスの定理」の巧妙な証明です。歴史の中には、独創的な証明、魔法のようなアイデア、天才的なインスピレーションが数多くありました。命題が証明されてしまえば、神にできることは何もありません。さて、ところで、「神は全能ではない」という証拠もあります。神は自分が持ち上げられない石を作ることはできません。
「数学的な証明には、非常に深い「洞察」が隠されていることがよくあります。多くの人が「フェルマーの最終定理」[1] の話を読んだことがあると思います。それを書き留めることはできません。」ワイルズがこの問題を解決するには、何世代にもわたる創意工夫が必要でした。上。最近では、ちょっと時代を感じさせる「ポアンカレ予想」や「ゴールドバッハ予想」、そして私が尊敬する中国の科学者、張宜棠が10年かけて熱心に研究した「ゴールドストン・ピンツ予想」など、 -Yıldırım」と「Bombieri-Friedlander-Iwaniec.」の証明「洞察」の後、「素数間の有界間隔」を証明しました [2]。
17世紀のライプニッツ以来、人々は天才的なひらめきに頼らずに証明を自動的に完了できる機械的手段を見つけることを夢見てきました。
20世紀初頭: 「証明」 == 「記号的推論」
19 世紀末、カントール、ブール、フレーゲ、ヒルベルト、ラッセル、ブラウ、ゲーデルらが形式論理の記号体系を定義しました。そして「証明」とは、形式論理という記号言語で書かれた推論プロセスのことです。ロジック自体は妥当なものでしょうか？論理自体は「自己矛盾しない」のでしょうか？論理的な推論自体は正しいのか、証明できるのか。これにより、数学者/論理学者/コンピューター科学者は、記号システム、構文と意味論、信頼性と完全性、再帰的と無限性を発明 (発見) するようになりました。 (素晴らしいストーリーのこの部分については、書籍「Logic Engine」[3] を参照してください)。
1910 年、ラッセルはホン (ズアン) フアン (トウ) の傑作『数学原理』を出版しました。この本の中で、ラッセルとホワイトヘッドは数学を完全に「形式化」しようとしました。そのような目標が達成できれば、すべての数学的結果は実証済みの方法で強固な基盤の上に構築されることになります。下の図は、『数学原理 (第 2 巻)』のページです。
このうち、110.643 は「1+1=2」という命題であり、この定理の証明は次のとおりです。 1+1 にはまだ証明が必要なのでしょうか?と疑問に思われるかもしれません。はい、『数学原理』という本では、数値 0、1、2、... が厳密に定義されており、「加算」、「乗算」、「等しい」も厳密に定義されている必要があり、推論のすべてのステップで必要になります。指摘されること。証明ってどういう意味ですか？証明は非常に面倒かもしれませんが、推論の各段階は厳密で正しいものです。この本の多くの証明は機械的なものです. 公理と推論規則に従って, 一種の証明構築が実行されます. 証明を探すことは人に渡され, そしてその人は一連の公理と推論の中で機械的に検索するようです.何も考えずに推測してルールを決めます。
人々は「定理の自動的な証明」を遠く離れていないように思えます。
残念ながら、ゲーデルは 1931 年に「ゲーデル不完全性定理」 [4] を証明し、チューリングは 1936 年にチューリング マシン停止問題の決定不可能性を証明しました [5]。これらの結果により、この何世紀にもわたる幻想に終止符が打たれました。公理系がどれほど巧妙に設計されていても、すべての真実を捉えることはできません。
Proof は、単なる厳密な推論ではなく、機械化するのが難しいと思われる創造的な思考を凝縮しています。証明には多くの「知識」が含まれており、あらゆるブレークスルーが私たちの認識を新しいレベルに引き上げます。それが「洞察」であれ、推論の過程で構築された「アルゴリズム」であれ、定理の証明の含意は定理自体の結論をはるかに超えていることがよくあります。
1960年代：「証明」==「手順」
半世紀後の1960年代、論理学者のハスケル・カリーとウィリアム・ハワードは、「論理システム」と「計算システム - ラムダ計算」における多くの「魔法の対応」を次々と発見し、後に「カリー・ハワード対応」と名付けられるようになりました。この発見により、誰もが「プログラムを書く」ことと「証明を書く」ということは、実は概念として完全に統一されていることに突然気づきました。その後 50 年間、関連する理論と技術の発展により、証明はもはや草稿にとどまらず、プログラムで表現できるようになりました。この同型写像は非常に興味深いものです: プログラムのタイプは証明の定理に対応し、サイクルは帰納法に対応します ... (ここで推奨される書籍: "Software Foundation" (Software Foundations 中国語訳) [6]) 。直観主義のフレームワークでは、証明とはアルゴリズムを構築することを意味し、アルゴリズムの構築は実際にコードを書くことになります。 (逆もまた真です。えーっと、コーダーによってコーディングされたものはコードではなく、数学的な証明です、:P)
現在、コンピュータサイエンスの分野では、多くの理論の証明が紙上のスケッチからコードの形に変わり、より一般的な「証明プログラミング言語」としては、Coq、Isabelle、Agdaなどが挙げられます。プログラミングを使用して証明を構築すると、証明の正しさのチェックがプログラムによって機械的に完了し、多くの反復作業がプログラムによって支援されます。コンピューター ソフトウェアと同様に、数学理論の証明の体系が段階的に構築されています。 1996 年 12 月、W. マキューンは自動定理証明ツール EQP を使用して 63 年前の数学的予想「ロンビン予想」を証明し、その後ニューヨーク タイムズ紙に「コンピューター数学の証明が推論力を示す」というタイトルの記事が掲載されました [7]。機械が人間の創造的思考を置き換えることができるかどうかの可能性について再び議論します。
機械支援の使用は、確かに数学者の思考がより未知の領域に到達するのに効果的に役立ちますが、「証明を探す」ことは依然として最も困難な仕事です。 「検証の証明」は単純かつ機械的で限定的な作業でなければなりません。これは自然な「非対称性」です。
1980年代：「証明」==「相互作用」
1985 年、ジョブズは Apple を辞めたばかりで、S. ゴールドワッサー博士は卒業後に MIT に来て、S. ミカリおよびラックフとコンピュータ サイエンスの歴史に記録される古典を共著しました。証明システムは複雑です。セックス」[8]。
彼らは「証明」という言葉を再解釈し、対話型証明システムの概念を提案しました。つまり、「理由」ではなく「相互作用」する 2 つのチューリング マシンを構築することで、命題が確率的に真であるかどうかを証明します。 「証明」の概念が再び拡張されました。
インタラクティブな証明の形式は、2 つ (またはそれ以上のチューリング マシン) の「対話スクリプト」、またはトランスクリプトです。そして、この対話プロセスには、明示的な「認証者」の役割と明示的な「検証者」の役割が存在します。このうち証明者は、命題が成立していることを検証者に証明すると同時に「それ以外の知識は一切開示しない」。これを「ゼロ知識証明」といいます。
副題
インタラクティブな証明
アリス: 方程式の解があることを証明したいのですが、w^3 - (w+1)^2 + 7 = 0 (方程式の解: w=3)
ボブ：分かった、聞いてるよ
アリス: でも、あなたがお金を払う気がない限り、x がいくらなのかは言いません。
ボブ: はい、でもまず方程式の解があることを証明しなければなりません、そうしたら私が支払います。
アリス: @#$%^& (ブラックテクノロジー)
ボブ：??????（ブラックテクノロジー）
アリス: &*#$@! (ブラックテクノロジー)
ボブ：??????（ブラックテクノロジー）
……（ブラックテクノロジーへ続く）
アリス：分かった、終わった
ボブ: そうですね、方程式の解はわかりますが、お金を払ったら答えを教えてくれませんか?
アリス: くだらない話はやめて、お金を払いましょう!
上記の例は「対話型証明」です。アリスが方程式 f(w) = 0 の解を知っていると仮定すると、どうすればアリスは w を知っているとボブに納得させることができるでしょうか?アリスは「ブラック・テクノロジー段階」でボブに多くの情報を伝えた。さて、重要な問題は、ボブはアリスが言った多くの情報から w が何であるかを推測できるか、それとも w に関する手がかりを分析できるかということです。ボブがこの能力を持っている場合、ボブはすでにこの貴重な情報を取得しているため、料金を支払う必要はありません。
アリスとボブの間の対話が「ゼロ知識」である場合、ボブは、w が f(w)=0 の解であることを除いて、w に関する他の情報を取得できないことに注意してください。これは非常に重要です、アリスの利益になります。
ここで「ゼロ知識証明」という用語を復習してください。英語では「Zero-Knowledge Proof」と呼ばれます。この言葉には 3 つの重要な部分があります。
ゼロ
証明する
証明する
すでに少し感じているかもしれませんが、それを解釈してみましょう。
ゼロ: アリスは、w に関する知識を「ゼロ」漏洩しました。つまり、知識は漏洩していません。
知識：ここではwを指します。
証拠: これは、アリスとボブの会話の「ブラック テクノロジー部分」です。
副題
ゼロ知識証明は何に役立ちますか?
ゼロ知識証明技術について言及するとき、多くの人は ZCash などの Monero などの匿名コインを思い浮かべます。実際、これらのコインはゼロ知識証明を非常によく普及させましたし、私自身もゼロ知識証明という言葉を ZCash を通じて初めて知りました。しかし、このテクノロジーをより深く理解すると、このテクノロジーの力はそれをはるかに超えていると深く感じます。
ゼロ知識証明テクノロジーは、データとコンピューティングの信頼性の問題を解決できます。
張三は100元持っていると言い、李斯は北京大学を卒業したと言い、王武は巴飛特と昼食を食べると言いました。証拠のない空虚な話、証拠を見せてください。
では、「ゼロ知識証明」はデータの信頼性をどのように解決できるのでしょうか?前回の記事「zkPoD: ブロックチェーン、ゼロ知識証明と形式検証、仲介者なしで公正な取引とゼロトラストを実現」 [9] で、「シミュレーション」という概念について言及しました。
ゼロ知識証明テクノロジーは、第三者を「シミュレート」して、特定の主張が信頼できることを確認できます。
言い換えれば、暗号化されたデータを受信すると、ゼロ知識証明が存在します。このゼロ知識証明は、「データに関する X の主張は真です」と言っていますが、これは天使が私たちの耳元で「データについての X の主張は真です」とささやいているのと同じです。
この X アサーションの場合、非常に柔軟であり、NP 複雑さのアルゴリズムにすることができます。専門用語では、データが X アサーションを満たすかどうかを判断するプログラム (多項式時間アルゴリズム) を作成できる限り、このアサーションはゼロ知識証明で表現できます。平たく言えば、データの判断が客観的である限り、ゼロ知識証明は適用可能です。
ゼロ知識証明のいくつかの用途:
データ プライバシーの保護: データ フォームには、多かれ少なかれ、公開したくない情報がいくつかあります。たとえば、その年の成績表など、自分の成績が合格であることを他の人に証明したいだけですが、私はそうではありません。自分のしたことを他の人に知られたくない。61 点や 62 点を獲得するのは恥ずかしいことだ。私は心臓病を持っていませんが、保険会社はそれを知る必要がありますが、私は保険会社に私の個人情報を知られたくないです。そうすれば、私は心臓発作を起こしていないことを保険会社に証明できますが、すべての医療記録を公開する必要はありません。私はビジネスを営んでおり、銀行から融資を受けたいと思っています。自分の事業が健全で返済能力があることを銀行に証明したいだけですが、銀行に企業秘密の一部を知られたくありません。
コンピューティング圧縮とブロックチェーン拡張: 多くのブロックチェーン拡張テクノロジーの中でも、Vitalik による zkSNARK テクノロジーの使用は、既存のイーサリアム フレームワークに数十倍のパフォーマンス向上をもたらすことができます。計算の証明があるため、同じ計算を何度も繰り返す必要がありません 従来のブロックチェーンアーキテクチャでは、署名検証、トランザクション合法性検証、スマートコントラクト検証など、同じ計算を何度も繰り返して実行します。これらの計算プロセスは、ゼロ知識証明技術によって圧縮できます。
エンドツーエンドの通信暗号化: ユーザーは相互にメッセージを送信できますが、サーバーがすべてのメッセージ レコードを取得することを心配する必要はありません。同時に、メッセージは、メッセージの送信元や送信目的などのサーバーの要件。
ID 認証: ユーザーは、秘密鍵を持っていること、またはユーザーだけが知っている秘密の答えを知っていることを Web サイトに対して証明できますが、Web サイトは知る必要はありませんが、Web サイトはこれを検証することでユーザーの身元を確認できます。ゼロ知識証明
分散ストレージ: サーバーは、データが適切に保管されており、データの内容を一切明らかにしないことをユーザーに証明できます。
信用記録: 信用記録は、ゼロ知識証明の利点を最大限に活用できるもう 1 つのフィールドであり、ユーザーは自分の信用記録を選択的に相手に提示できます。
オンラインデジタル商品のための完全に公正な取引プロトコルを構築します[9]。
副題
例: 地図の三重色付け問題
古典的な問題、地図の 3 色問題について話しましょう。隣接する 2 つの領域が異なる色になるように、マップを 3 色で色付けする方法。この「地図三色問題」を「接続グラフ頂点三色問題」に変換します。各領域に首都 (ノード) があると仮定し、隣接するノードを接続すると、マップの色付け問題が接続されたグラフの頂点の色付け問題に変換されます。
対話プロトコルを設計してみましょう。
「認証者」アリス
「検証者」ボブ
アリスは地図の 3 つの色に対する答えを手に持っています。下の写真を参照してください。このグラフには合計 6 つの頂点と 9 つの辺があります。
ここで、アリスは自分が答えを持っていることをボブに証明したいと考えていますが、ボブには答えを知られたくないのです。アリスはどうするつもりですか？
アリスはまず、染めた絵に「変換」を実行し、すべての緑をオレンジに変える、すべての青を緑に変える、すべての緑をオレンジに変えるなど、色を大きく変える必要があります。その後、アリスは新しい色付けの答えを得て、新しいグラフの各頂点を紙で覆い、それをボブに見せました。
下の図を見てください。この時点で、ボブは行動を起こそうとしています (下の図を参照)。彼は「サイド」をランダムに選択したいと考えています。これはランダムであることに注意してください。アリスは乱数を予測させません。前進。
ボブが下の端を選んでアリスに告げたとします。
このとき、アリスはこの辺の両端の紙片を取り出してボブに確認してもらいますが、ボブは 2 つの頂点の色が異なることに気づき、このテストは同型であると考えます。この時点で、ボブはグラフの一部しか見ていませんが、グラフの残りの頂点の色が問題ないと確信できますか?これでは十分ではないと感じているはずです。おそらくアリスは正しく理解したのではないでしょうか?露出されていない他の頂点はランダムに色付けされる場合があります。
それは問題ではありません、ボブはアリスにもう一度それをするように頼むことができます、下の写真を参照してください
アリスは再び色を変更し、青を紫に、緑から茶色に、オレンジからグレーに変更し、すべての頂点を紙で覆います。次に、ボブは別のエッジを選択します。たとえば、上の図のように、垂直エッジを選択し、アリスに紙を開いて見てもらいます。ボブがこのエッジの両端の頂点の色が異なることに気付いた場合、次のようにします。それからボブは時間が少しよどんだので、おそらくアリスはこの色に対する答えを本当に持っているのかもしれません。しかし、2 回ではまだ不十分で、ボブはあと数回やりたいと考えています。
そして、これらの 3 つのステップを何度も繰り返すと、アリスがボブを騙して首尾よく騙せる確率は指数関数的に減少します。 n ラウンド後のアリスの不正行為の確率は次のようになるとします。
ここで |E| はグラフ内のすべてのエッジの数であり、n が十分に大きい場合、この確率 Pr は非常に非常に小さくなり、「無視できる」ものになります。
副題
情報と知識
インフォメーション「インフォメーション」
知識「知識」
地図の 3 色塗り分け問題のインタラクティブな証明では、何度もインタラクションを繰り返した後、ボブは多くの情報を取得しますが、これはアリスがボブに大量の乱数を送信するようなもので、ボブはそれ以上のことを「知っている」わけではありません。たとえば、アリスがボブに「1+1=2」と言った場合、ボブはこの情報を取得しますが、この事実は誰もが知っているため、ボブはそれ以上の「知識」を取得しません。
アリスがボブに 2^2^41-1 という数字は素数であると伝えた場合、その数字が素数かどうかを判断するには多くの計算能力が必要となるため、これは明らかに「知識」です。
アリスがボブに緑色の頂点が合計 2 つあると伝えた場合、ボブは貴重な「知識」を獲得したことになります。なぜなら、ボブは得たばかりの情報に基づいて、チューリング マシンを使用して 3 つの頂点をより短い時間で解くことができるからです。汚れの問題。アリスがボブに、左端の頂点の色がオレンジであることを明らかにした場合、明らかに、この「情報」はボブの問題解決に実質的に役立ちません。
対話プロセス中にボブが取得した「情報」が、アリスの秘密を直接解読するボブの能力を向上させるのに役立つ場合、ボブは「知識を獲得した」と言えると定義してみることができます。知識という言葉の定義はボブの計算能力に関係していることがわかりますが、情報がボブの計算能力を向上させない場合、その情報は「知識」とは言えません。例えば、アリスとボブのやりとりにおいて、アリスは毎回コインを投げ、その結果をボブに伝えるのですが、情報という観点から見ると、ボブが得られる情報は単なる「出来事」ですが、ボブは何の「知識」も得られません。なぜなら、ボブは完全に自分でコインを投げることができるからです。
以下は、書籍「Foundations of Cryptography - Basic Tools」[10] の概要を引用しています。
「知識」は「計算難易度」と関係しますが、「情報」は関係ありません
「知識」は公に知られているものに関係し、「情報」は主に部分的に公にされているものに関係します。
副題
検証可能な計算と回路の充足性の問題
上の地図上の 3 色の問題を見て、これは単なる学術的な問題であり、現実の問題とどのように関連付けられると感じますか?マップ 3 色付け問題は、「計算理論」の用語である NP-Complete 問題です。 「回路充足問題」と呼ばれるもう 1 つの問題も、NP 完全問題です。 NP-Complete は問題の一種で、その解法過程は多項式時間で完了することが難しい、つまり「解くのが難しい」が、解を検証する過程は多項式時間で完了できる、つまり「検証が簡単」である」。
では、回路とは何でしょうか？以下に 3 つの異なる「演算回路」を示します。
回路は加算ゲートや乗算ゲートを含む多くのゲートで構成されていることがわかります。各ゲートには、いくつかの入力ピンといくつかの出力ピンがあります。各ゲートは加算演算または乗算演算を実行します。それほど単純に思わないでください。私たちが通常実行するコード (無限ループなし) は、算術回路で表すことができます。
これはどういう意味ですか？ 「ゼロ知識証明」と「回路充足性問題」を組み合わせて、データプライバシー保護問題を解決してみましょう。
次に、シナリオについて考えてください。ボブがアリスにコード P と入力 x を与え、アリスにそれを 1 回実行するように依頼し、その結果をボブに伝えます。おそらくこの計算にはリソースを消費する必要があるため、ボブは計算プロセスをアリスに外注します。その後、アリスは再度実行し、結果 y を得ました。それからボブに伝えてください。ここで次のような質問が生じます。
コードを実行せずに、コード P の実行結果が y になるはずだとボブに信じさせるにはどうすればよいでしょうか?
ここは思考の時間です、誰もが 5 分間考えます...
（5分後……）
アリスさんの方法の 1 つは、計算プロセス全体を携帯電話で撮影することで、このビデオには、コンピューターの CPU、メモリ、演算プロセス全体における各トランジスタの状態が含まれます。そうするのは明らかに非現実的です。それでは、より実現可能な解決策はあるのでしょうか?
答えは、ボブがプログラム P を完全に等価な演算回路に変換し、その回路をアリスに渡すというものです。アリスは回路を計算するだけでよく、回路規模がそれほど大きくなければ、その過程を携帯電話で写真に撮ったり、紙に書き留めたりすることができます。アリスはパラメータ 6 を回路に入力し、回路の動作中にゲートに接続されているすべてのピンの値を記録するだけです。そして、最後の回路出力ピンの値が y に等しい場合、ボブはアリスが計算を実行したことを確信できます。アリスは回路のすべてのゲートの入力と出力を紙に書いてボブに渡す必要があります。この紙は計算の証明です。
このようにして、ボブは回路を再計算することなく、この紙に書かれた証明が正しいかどうかを検証できます。検証プロセスは非常に簡単です。
ボブは、各ゲートの入力と出力が加算方程式または乗算方程式を満たすことができるかどうかを順番にチェックします。
たとえば、ゲート No. 1 は加算ゲートで、その 2 つの入力は 3、4、出力は 7 であるため、このゲートの計算が正しいことは簡単にわかります。ボブはすべてのドアをチェックすると、次のことを確認できます。
アリスは実際に計算をしました、彼女は不正行為をしませんでした。
この論文の内容は、演算回路Pを「満足させる」解「Solution」です。
いわゆる回路充足性とは、回路を満たす解が存在することを意味します。この解の出力値が特定の値に等しい場合、この解は回路の計算プロセスを「表す」ことができます。
アリスの場合、ボブがこのように検証すれば、不正行為の余地はまったくありません。しかし、この方法には明らかに欠点があります。
デメリット 1: 回路が比較的大きい場合、証明は非常に大きくなり、ボブが証明をチェックする作業負荷も非常に大きくなります。
欠点 2: 検証プロセス中、ボブは入力を含む回路動作の詳細をすべて知っています。
ブラックテクノロジー
先ほどのアリスとボブのシーンにいくつかの変更を加えてみましょう。アリス自身がオンライン バンキングのパスワードなどの秘密を持っているとします。そしてボブは、アリスのオンライン バンキングのパスワードの長さが 20 文字であるかどうかを知りたいと考えています。しかし、アリスは少し考えて、パスワードの長さは大きな問題ではないはずだと言いました。このとき、ボブは文字列の長さを計算するコードを回路Qに変換し、アリスに送信する。アリスは回路Qで自分のパスワードを計算し、回路のすべてのゲートのピンをボブに送り、計算結果20を持ってきました。
待ってください、これは問題があります。ボブは回路動作の内部詳細をすべて取得した後、パスワードを知らないのですか?はい、アリスには明らかにそれができません。それで、アリスは何をすべきでしょうか？
答えは、多くの方法があるということです。ブロックチェーン テクノロジーを愛する読者は、zkSNARK[11]、zkSTARK[12]、BulletProof[13]、およびいくつかの比較的小規模なテクノロジーに最も精通しており、これらはすべて、Alice がそれを行うのに役立ちます。
ゼロ知識の方法で、アリスは回路を計算し、秘密の入力を使用したことをボブに証明します。
言い換えれば、これらの「ゼロ知識回路充足性証明プロトコル」は、アリスに、オンライン バンキングのパスワードの長さが 20 であることをボブに証明するための強力な武器を提供し、それ以外に、ボブは他の有用な情報を取得できなくなります。オンライン バンキングのパスワードに加えて、理論的には、アリスは自分の個人データのいくつかの特徴をボブに証明できますが、他の情報は明らかにしません。
「ゼロ知識回路充足性証明プロトコル」は、プライバシー/機密データを保護するための最も直接的な技術を提供します
最後に書きます
最後に書きます
それが微妙な数論の定理であっても、三色写像の問題であっても、あるいは回路充足可能性の問題であっても。存在を証明することに何の意味があるのでしょうか？すべての証明は、「証明」と「検証」の間の「非対称性」を体現しています。証明は、数百年かかった「フェルマーの最終定理」であれ、ビットコインの POW 証明であれ、非常に計算力や精神力を消耗するアクティビティである可能性があり、これらの証明には、証明を見つけるプロセスに費やされる時間が凝縮されています。プロセスは非現実的に複雑になる可能性があり、場合によっては天才的な才能を発揮する必要があります。そして、検証プロセスは、非常に単純で機械的で、（多項式の）有効時間内に終了可能なアクティビティである必要があります（またはそうすべきです）。ある意味、この非対称性は証明の重要性をまさに体現しており、ゼロ知識証明の価値を示しています。
「証明」は大まかに言うと「論理」の産物ですが、「論理」と「計算」は切っても切れない関係にあります。表現、対話型計算。これは興味深いですが、より大きな哲学的な問題です。
参考文献
参考文献
[1] Simon, Singer, Xue Mi. フェルマーの最終定理: 世界の賢者を 358 年間困惑させた謎 [M]. 上海翻訳出版社、1998 年。
[2] Alec Wilkinson. The Pursuit of Beauty: Yitang Zhang solves a pure-math mystery. The New Yorker. Feb. 2015.
[3] Martin、Davis、Zhang Butian、論理のエンジン [M]、湖南科学技術出版、2012 年。
[4] Raymond Smullyan. Gödel's Incompleteness Theorems, Oxford Univ.Press. 1991.
[5] Turing, Alan. "On computable numbers, with an application to the Entscheidungsproblem." Proceedings of the London mathematical society 2.1 (1937): 230-265.
[6] Pierce, Benjamin C., et al. "Software foundations."中国語訳：<https://github.com/Coq-zh/SF-zh
[7] Kolata, Gina. "Computer math proof shows reasoning power." Math Horizons 4.3 (1997): 22-25.
[8] Goldwasser, Shafi, Silvio Micali, and Charles Rackoff. "The knowledge complexity of interactive proof systems." SIAM Journal on computing 18.1 (1989): 186-208.
[9] zkPoD: ブロックチェーン、ゼロ知識証明と形式的検証、仲介者なしの公正な取引とゼロトラストを実現. Ambi Lab. 2019.
[10] Oded, Goldreich. "Foundations of cryptography basic tools." (2001).
[11] Gennaro, Rosario, et al. "Quadratic span programs and succinct NIZKs without PCPs." AnnualInternational Conference on the Theory and Applications of Cryptographic Techniques. Springer Berlin, Heidelberg, 2013.
[12] Ben-Sasson, Eli, et al. "Scalable, transparent, and post-quantum secure computational integrity." IACR Cryptology ePrint Archive 2018 (2018): 46.
[13] Bünz, Benedikt, et al. "Bulletproofs: Short proofs for confidential transactions and more." 2018IEEE Symposium on Security and Privacy (SP). IEEE, 2018.
IOS
Android