論文の概要: Formal Verification of the Sumcheck Protocol
- arxiv url: http://arxiv.org/abs/2402.06093v1
- Date: Thu, 8 Feb 2024 23:01:32 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-18 07:38:15.339721
- Title: Formal Verification of the Sumcheck Protocol
- Title（参考訳）: サムチェックプロトコルの形式的検証
- Authors: Azucena Garvía Bosshard, Jonathan Bootle, Christoph Sprenger,
- Abstract要約: 1992年に導入されたsumcheckプロトコルは、多くの確率的証明システムの重要な構成要素である対話的証明である。
本稿では,対話型定理証明器Isabelle/HOLを用いた要約プロトコルのセキュリティ解析について述べる。
- 参考スコア（独自算出の注目度）: 2.3591022864158067
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: The sumcheck protocol, introduced in 1992, is an interactive proof which is a key component of many probabilistic proof systems in computational complexity theory and cryptography, some of which have been deployed. However, none of these proof systems based on the sumcheck protocol enjoy a formally-verified security analysis. In this paper, we make progress in this direction by providing a formally verified security analysis of the sumcheck protocol using the interactive theorem prover Isabelle/HOL. We follow a general and modular approach. First, we give a general formalization of public-coin interactive proofs. We then define a generalized sumcheck protocol for which we axiomatize the underlying mathematical structure and we establish its soundness and completeness. Finally, we prove that these axioms hold for multivariate polynomials, the original setting of the sumcheck protocol. Our modular analysis facilitates formal verification of sumcheck instances based on different mathematical structures with little effort, by simply proving that these structures satisfy the axioms. Moreover, the analysis supports the development and formal verification of future cryptographic protocols using the sumcheck protocol as a building block.
- Abstract（参考訳）: 1992年に導入されたsumcheckプロトコルは、計算複雑性理論や暗号における多くの確率的証明システムの鍵となる、対話的な証明である。
しかし、この総括プロトコルに基づく証明システムには、公式に検証されたセキュリティ分析が存在しない。
本稿では,対話型定理証明器Isabelle/HOLを用いて,要約プロトコルの正式なセキュリティ解析を行うことにより,この方向を進展させる。
私たちは汎用的でモジュール化されたアプローチに従います。
まず、公開コインインタラクティブな証明を一般化する。
次に、基礎となる数学的構造を公理化し、その健全性と完全性を確立するための一般化された総括プロトコルを定義する。
最後に、これらの公理が、和チェックプロトコルの元々の設定である多変量多項式に対して成り立つことを証明した。
我々のモジュラー解析は、これらの構造が公理を満たすことを単純に証明することによって、異なる数学的構造に基づく要約インスタンスの形式的検証を容易にする。
さらに、この分析は、sumcheckプロトコルをビルディングブロックとして使用して、将来の暗号プロトコルの開発と形式検証を支援する。
関連論文リスト
- Quantum Rewinding for IOP-Based Succinct Arguments [45.5096562396529]
我々は、ベクトルコミットメントスキームが崩壊しているとき、BCS変換のインタラクティブな変種が量子敵に対する標準モデルで安全であることを証明した。
その結果、量子後安全な簡潔な議論の標準モデルを得ることができ、その複雑さを最もよく知ることができる。
論文 参考訳（メタデータ） (2024-11-08T06:33:08Z) - Protocols for Quantum Weak Coin Flipping [0.1499944454332829]
弱いコインフリップは重要な暗号プリミティブである。
我々は関連するユニタリ作用素の正確な構成を与える。
本稿では, 明快なコインフリッププロトコルの構築について述べる。
論文 参考訳（メタデータ） (2024-02-24T16:52:54Z) - Prototype-based Aleatoric Uncertainty Quantification for Cross-modal
Retrieval [139.21955930418815]
クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。
しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。
本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
論文 参考訳（メタデータ） (2023-09-29T09:41:19Z) - Entropy Accumulation under Post-Quantum Cryptographic Assumptions [4.416484585765028]
デバイス非依存(DI)量子プロトコルでは、セキュリティステートメントは量子装置の特性を損なう。
本稿では,量子情報理論のツールの組み合わせを利用して,そのようなプロトコルの安全性を証明するフレキシブルなフレームワークを提案する。
論文 参考訳（メタデータ） (2023-07-02T12:52:54Z) - CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。
主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。
理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
論文 参考訳（メタデータ） (2023-05-20T11:26:51Z) - Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムを検証するために使用された。
Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有である。
論文 参考訳（メタデータ） (2023-04-05T01:21:00Z) - DeepSec: Deciding Equivalence Properties for Security Protocols -- Improved theory and practice [8.735998284944436]
我々はこの検証問題の理論と実践に貢献する。
静的同値、トレース同値およびラベル付き二相性のための新しい複雑性結果を確立する。
我々の手順は、多種多様な暗号プリミティブに対して、トレース同値とラベル付き二相性を決定する最初の方法である。
論文 参考訳（メタデータ） (2022-11-06T22:01:04Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳（メタデータ） (2022-08-12T17:03:50Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z) - Revisiting the Sample Complexity of Sparse Spectrum Approximation of
Gaussian Processes [60.479499225746295]
本稿では,ガウス過程に対して,パラメータ空間全体に対して同時に保持可能な保証付きスケーラブルな近似を導入する。
我々の近似は、スパーススペクトルガウス過程(SSGP)のための改良されたサンプル複雑性解析から得られる。
論文 参考訳（メタデータ） (2020-11-17T05:41:50Z) - A refinement of Reznick's Positivstellensatz with applications to
quantum information theory [72.8349503901712]
ヒルベルトの17番目の問題において、アルティンはいくつかの変数の任意の正定値が2つの平方和の商として書けることを示した。
レズニックはアルティンの結果の分母は常に変数の平方ノルムの$N$-次パワーとして選択できることを示した。
論文 参考訳（メタデータ） (2019-09-04T11:46:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。