論文の概要: Reusable Formal Verification of DAG-based Consensus Protocols
- arxiv url: http://arxiv.org/abs/2407.02167v1
- Date: Tue, 2 Jul 2024 11:19:12 GMT
- ステータス: 処理完了
- システム内更新日: 2024-07-03 15:45:15.792911
- Title: Reusable Formal Verification of DAG-based Consensus Protocols
- Title（参考訳）: DAGベースの合意プロトコルの再利用可能な形式検証
- Authors: Nathalie Bertrand, Pranav Ghorpade, Sasha Rubin, Bernhard Scholz, Pavle Subotic,
- Abstract要約: DAGベースのコンセンサスプロトコルは、エネルギーフットプリントの削減とセキュリティ向上のために、ブロックチェーン企業によって採用されている。
本稿では,2つのDAGプロトコルの安全仕様について述べる。
- 参考スコア（独自算出の注目度）: 8.277981465630377
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: DAG-based consensus protocols are being adoption by blockchain companies to decrease energy footprints and improve security. A DAG-based consensus protocol collaboratively constructs a partial order of blocks of transactions and produces linearly ordered blocks. The ubiquity and strategic importance of blockchains call for formal proof of the correctness of key components, namely, consensus protocols. This paper presents a safety-proven formal specification of two DAG-based protocols. Our specification highlights several dissemination, DAG construction, and ordering variations that can be combined to express the two protocols. The formalization requires a refinement approach for modeling the consensus. In an abstract model, we first show the safety of DAG-based consensus on leader blocks and then further refine the specification to encompass all blocks for all processes. The TLA+ specification for a given protocol consists of 492-732 lines, and the proof system TLAPS verifies 2025-2294 obligations in 6-8 minutes.
- Abstract（参考訳）: DAGベースのコンセンサスプロトコルは、エネルギーフットプリントの削減とセキュリティ向上のために、ブロックチェーン企業によって採用されている。
DAGベースのコンセンサスプロトコルは、トランザクションのブロックの部分的な順序を協調的に構築し、線形に順序付けられたブロックを生成する。
ブロックチェーンの普遍性と戦略的重要性は、キーコンポーネント、すなわちコンセンサスプロトコルの正しさを正式に証明することを要求する。
本稿では,2つのDAGプロトコルの安全仕様について述べる。
本仕様では,2つのプロトコルを組み合わせて表現可能な,いくつかの分散化,DAGの構成,順序付けのバリエーションを強調している。
形式化はコンセンサスをモデル化するために洗練されたアプローチを必要とする。
抽象モデルでは、まず、DAGベースのリーダブロックに対するコンセンサスの安全性を示し、次に、すべてのプロセスのすべてのブロックを包含するように仕様をさらに洗練する。
与えられたプロトコルの TLA+ 仕様は 492-732 行で構成され、証明システム TLAPS は 6-8 分で 2025-2294 の義務を検証している。
関連論文リスト
- 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) - A Security Verification Framework of Cryptographic Protocols Using
Machine Learning [0.0]
機械学習を用いた暗号プロトコルのセキュリティ検証フレームワークを提案する。
ランダムなプロトコルを自動的に生成し、セキュリティラベルを割り当てることで、任意に大規模なデータセットを作成する。
提案手法を実用的な暗号プロトコルの検証に適用して評価する。
論文 参考訳（メタデータ） (2023-04-26T02:37:43Z) - Byzantine-Robust Federated Learning with Optimal Statistical Rates and
Privacy Guarantees [123.0401978870009]
ほぼ最適な統計率を持つビザンチン・ロバスト・フェデレーション学習プロトコルを提案する。
競合プロトコルに対してベンチマークを行い、提案プロトコルの実証的な優位性を示す。
我々のバケットプロトコルは、プライバシー保証手順と自然に組み合わせて、半正直なサーバに対するセキュリティを導入することができる。
論文 参考訳（メタデータ） (2022-05-24T04:03:07Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。