論文の概要: Reusable Formal Verification of DAG-based Consensus Protocols

• arxiv url: http://arxiv.org/abs/2407.02167v2
• Date: Tue, 18 Mar 2025 16:10:48 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-19 14:12:31.415967
• Title: Reusable Formal Verification of DAG-based Consensus Protocols
• Title（参考訳）: DAGベースの合意プロトコルの再利用可能な形式検証
• Authors: Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, Pavle Subotic,
• Abstract要約: 本稿では,DAGに基づく5つのコンセンサスプロトコルの安全性検証仕様を提案する。 DAG-Rider、Cordial Miners、Hashgraph、Eventualous BullSharkの4つのプロトコルがこの文献で十分に確立されている。 我々は、プロトコルの指定と証明書作成にTLA+を使用し、TLAPS証明システムは証明を自動的にチェックする。
• 参考スコア（独自算出の注目度）: 8.277981465630377
• License:
• Abstract: Blockchains use consensus protocols to reach agreement, e.g., on the ordering of transactions. DAG-based consensus protocols are increasingly adopted by blockchain companies to reduce energy consumption and enhance security. These protocols collaboratively construct a partial order of blocks (DAG construction) and produce a linear sequence of blocks (DAG ordering). Given the strategic significance of blockchains, formal proofs of the correctness of key components such as consensus protocols are essential. This paper presents safety-verified specifications for five DAG-based consensus protocols. Four of these protocols -- DAG-Rider, Cordial Miners, Hashgraph, and Eventual Synchronous BullShark -- are well-established in the literature. The fifth protocol is a minor variation of Aleph, another well-established protocol. Our framework enables proof reuse, reducing proof efforts by almost half. It achieves this by providing various independent, formally verified, specifications of DAG construction and ordering variations, which can be combined to express all five protocols. We employ TLA+ for specifying the protocols and writing their proofs, and the TLAPS proof system to automatically check the proofs. Each TLA+ specification is relatively compact, and TLAPS efficiently verifies hundreds to thousands of obligations within minutes. The significance of our work is two-fold: first, it supports the adoption of DAG-based systems by providing robust safety assurances; second, it illustrates that DAG-based consensus protocols are amenable to practical, reusable, and compositional formal methods.
• Abstract（参考訳）: ブロックチェーンはコンセンサスプロトコルを使用して、トランザクションの順序に関する合意に達する。 DAGベースのコンセンサスプロトコルは、エネルギー消費の削減とセキュリティ向上のために、ブロックチェーン企業によってますます採用されている。 これらのプロトコルは、ブロックの部分順序(DAG構成)を協調的に構築し、ブロックの線形列(DAG順序)を生成する。 ブロックチェーンの戦略的重要性を考えると、コンセンサスプロトコルのような重要なコンポーネントの正しさの正式な証明は不可欠である。 本稿では,DAGに基づく5つのコンセンサスプロトコルの安全性検証仕様を提案する。 DAG-Rider、Cordial Miners、Hashgraph、Eventual Synchronous BullSharkの4つのプロトコルがこの文献でよく確立されている。 第5のプロトコルは、もう1つの確立されたプロトコルであるAlephの小さなバリエーションである。 我々のフレームワークは、証明の再利用を可能にし、証明の労力をほぼ半分に削減する。 これは、DAGの構成と順序付けのバリエーションの様々な独立した公式な仕様を提供することによって実現され、5つのプロトコルすべてを表現するために組み合わせることができる。 我々は、プロトコルの指定と証明書作成にTLA+を使用し、TLAPS証明システムは証明を自動的にチェックする。 各TLA+仕様は比較的コンパクトであり、TLAPSは数分で数百から数千の義務を効率的に検証する。 第1に,DAGベースのコンセンサスプロトコルが実用的,再利用可能な,構成的な形式的手法に適応可能であることを示す。

関連論文リスト

• Automated Selfish Mining Analysis for DAG-based PoW Consensus Protocols [0.0]
  利己的なマイニングは、仕事の証明プロトコルにおける報酬を最大化するための戦略的なルール破りである。 本稿では,Proof-of-Work,GhostDAG,Parallel Proof-Workなど,幅広いプロトコルをカバーする汎用攻撃モデルを提案する。
  論文  参考訳（メタデータ） (2025-01-18T21:57:02Z)
• Quantum digital signature based on single-qubit without a trusted third-party [45.41082277680607]
  我々は、よりセキュリティを向上させるために、量子ビット技術のみを頼りにすることなく、新しい量子デジタル署名プロトコルを提案する。 また,このプロトコルは,非対称性,不確定性,拡張性など,他の重要な安全特性を満足する。
  論文  参考訳（メタデータ） (2024-10-17T09:49:29Z)
• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。 しきい値暗号システムに対する既存のアプローチは、しきい値暗号プロトコルを実行するための少なくとも1つのメッセージ遅延の遅延オーバーヘッドを導入している。 しきい値が狭いブロックチェーンネイティブのしきい値暗号システムに対して,このオーバーヘッドを取り除く機構を提案する。
  論文  参考訳（メタデータ） (2024-07-16T20:53:04Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
  論文  参考訳（メタデータ） (2024-05-09T19:57:59Z)
• Security of hybrid BB84 with heterodyne detection [0.0]
  量子鍵分布(QKD)は物理学の法則に基づく永続的なセキュリティを約束する。 最近のハイブリッドQKDプロトコルは、両方のカテゴリの利点を活用するために導入されている。 我々は2021年にQiによって導入されたプロトコルの厳密なセキュリティ証明を提供し、そこでは情報を離散変数に符号化する。
  論文  参考訳（メタデータ） (2024-02-26T19:00:01Z)
• Coding-Based Hybrid Post-Quantum Cryptosystem for Non-Uniform Information [53.85237314348328]
  我々は、新しいハイブリッドユニバーサルネットワーク符号化暗号(NU-HUNCC)を導入する。 NU-HUNCCは,リンクのサブセットにアクセス可能な盗聴者に対して,個別に情報理論的に保護されていることを示す。
  論文  参考訳（メタデータ） (2024-02-13T12:12:39Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Provably Secure Commitment-based Protocols over Unauthenticated Channels [0.0]
  我々は、認証された交換のための既存のモデルと必ずしも一致しない可能性のあるプロトコルをカバーするための理論的なセキュリティフレームワークを構築している。 本稿では,両当事者間の共通秘密を確立するためのコミットベースのプロトコルをいくつか提案し,その非認証チャネルに対する抵抗性について検討する。 これは、プロトコル自体のセキュリティの堅牢性、およびMan-in-the-Middle攻撃に対する堅牢性を分析することを意味する。
  論文  参考訳（メタデータ） (2023-07-28T10:35:35Z)
• Data post-processing for the one-way heterodyne protocol under composable finite-size security [62.997667081978825]
  本研究では,実用的連続可変(CV)量子鍵分布プロトコルの性能について検討する。 ヘテロダイン検出を用いたガウス変調コヒーレント状態プロトコルを高信号対雑音比で検討する。 これにより、プロトコルの実践的な実装の性能を調べ、上記のステップに関連付けられたパラメータを最適化することができる。
  論文  参考訳（メタデータ） (2022-05-20T12:37:09Z)
• Round-robin differential phase-time-shifting protocol for quantum key distribution: theory and experiment [58.03659958248968]
  量子鍵分布(QKD)は、遠隔者間で共通の暗号鍵の確立を可能にする。 近年,信号の乱れの監視を回避できるQKDプロトコルが提案され,初期の実験で実証されている。 我々は,ラウンドロビン差動位相シフトプロトコルのセキュリティ証明を,集団攻撃シナリオにおいて導出する。 その結果,RRDPTSプロトコルは高い量子ビット誤り率の条件下で,RDPSと比較して高い秘密鍵レートが得られることがわかった。
  論文  参考訳（メタデータ） (2021-03-15T15:20:09Z)
• Twin-field quantum digital signatures [4.503555294002338]
  デジタルシグネチャ(Digital signature)は、情報セキュリティ、特にID認証において重要な技術である。 量子デジタルシグネチャ(QDS)は、情報理論のセキュリティなど、より高度なセキュリティを提供する。
  論文  参考訳（メタデータ） (2020-03-25T08:04:59Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。