論文の概要: Model Checking the Security of the Lightning Network

• arxiv url: http://arxiv.org/abs/2505.15568v1
• Date: Wed, 21 May 2025 14:22:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-22 15:42:59.69665
• Title: Model Checking the Security of the Lightning Network
• Title（参考訳）: 雷ネットワークのセキュリティのモデルチェック
• Authors: Matthias Grundmann, Hannes Hartenstein,
• Abstract要約: Lightning NetworkはBitcoin用に構築された支払いチャネルネットワークで、すでに使われている。 我々はTLA+でプロトコルを定式化し、正直なユーザーが正しいバランスを取り戻すことが保証されるセキュリティ特性を正式に規定する。 証明を用いて検証する2つの改良ステップを用いて、Lightning Networkのモデルチェックを可能にする。
• 参考スコア（独自算出の注目度）: 0.7366405857677227
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Payment channel networks are an approach to improve the scalability of blockchain-based cryptocurrencies. The Lightning Network is a payment channel network built for Bitcoin that is already used in practice. Because the Lightning Network is used for transfer of financial value, its security in the presence of adversarial participants should be verified. The Lightning protocol's complexity makes it hard to assess whether the protocol is secure. To enable computer-aided security verification of Lightning, we formalize the protocol in TLA+ and formally specify the security property that honest users are guaranteed to retrieve their correct balance. While model checking provides a fully automated verification of the security property, the state space of the protocol's specification is so large that model checking becomes unfeasible. We make model checking the Lightning Network possible using two refinement steps that we verify using proofs. In a first step, we prove that the model of time used in the protocol can be abstracted using ideas from the research of timed automata. In a second step, we prove that it suffices to model check the protocol for single payment channels and the protocol for multi-hop payments separately. These refinements reduce the state space sufficiently to allow for model checking Lightning with models with payments over up to four hops and two concurrent payments. These results indicate that the current specification of Lightning is secure.
• Abstract（参考訳）: 支払いチャネルネットワークは、ブロックチェーンベースの暗号通貨のスケーラビリティを改善するためのアプローチである。 Lightning NetworkはBitcoin用に構築された支払いチャネルネットワークで、すでに使われている。 ライトニングネットワークは金銭的価値の移転に使用されるため、敵の参加者の存在下でのセキュリティを検証する必要がある。 Lightningプロトコルの複雑さは、プロトコルがセキュアかどうかを評価するのを難しくする。 コンピュータ支援によるLightningのセキュリティ検証を可能にするため、TLA+でプロトコルを形式化し、正直なユーザが正しいバランスを取り戻すことが保証されるセキュリティ特性を正式に指定する。 モデルチェックは、セキュリティプロパティの完全な自動検証を提供するが、プロトコルの仕様の状態空間が非常に大きく、モデルチェックが不可能になる。 証明を用いて検証する2つの改良ステップを用いて、Lightning Networkのモデルチェックを可能にする。 最初のステップでは、プロトコルで使用される時間のモデルが、タイムドオートマトンの研究のアイデアを用いて抽象化できることを実証する。 第2のステップでは、単一支払いチャネルのプロトコルとマルチホップ支払いのプロトコルを別々にモデル化するのに十分であることを示す。 これらの改良により、最大4つのホップと2つの同時支払いを備えたモデルでLightningをモデルチェックできる十分な状態空間が縮小される。 これらの結果は、現在のLightningの仕様が安全であることを示している。

関連論文リスト

• A Formally Verified Lightning Network [0.0]
  われわれは、Lightning Network(LN)が常に誠実なユーザーの資金を保護していることを示すために、正式な検証を行っている。 我々は、LNのカスタム実装(単純化)を提供し、所望のセキュリティ目標を表現し、初めて、彼らがすべてのシナリオで維持されているというマシンチェック可能な証明を提供する。
  論文  参考訳（メタデータ） (2025-03-10T11:33:22Z)
• Formal Model Guided Conformance Testing for Blockchains [1.4838910416636741]
  本稿では,プロトコルの形式モデルを用いたプロトコル適合性テストを行うフレームワークを提案する。 私たちのフレームワークは、トレースジェネレータとチェッカーとしてコンポーネントを使用する2つの補完的なコンポーネントで構成されています。
  論文  参考訳（メタデータ） (2025-01-15T03:20:13Z)
• BlockFound: Customized blockchain foundation model for anomaly detection [47.04595143348698]
  BlockFoundは、異常なブロックチェーントランザクション検出のためのカスタマイズされた基盤モデルである。 ブロックチェーントランザクションのユニークなデータ構造をモデル化するための、一連のカスタマイズデザインを紹介します。 BlockFoundは、Solana上の異常なトランザクションを高精度に検出する唯一の方法である。
  論文  参考訳（メタデータ） (2024-10-05T05:11:34Z)
• The Latency Price of Threshold Cryptosystem in Blockchains [52.359230560289745]
  本稿では,Byzantine-fault Tolerant(BFT)コンセンサスプロトコルを用いた,しきい値暗号とブロックチェーンのクラス間の相互作用について検討する。 Aptosのメインネットからの測定によると、楽観的なアプローチは遅延オーバーヘッドを71%削減する。
  論文  参考訳（メタデータ） (2024-07-16T20:53:04Z)
• Payout Races and Congested Channels: A Formal Analysis of Security in the Lightning Network [8.397189036839956]
  Lightning Networkは、Bitcoinのスケーラビリティ問題を解決するために設計された支払いチャネルネットワークである。 いくつかの脆弱性が手作業で発見されたが、これまでLightning Networkのセキュリティを体系的に分析する作業はほとんど行われていない。 我々は、正式な手法を用いて、Lightning Networkのセキュリティを分析するための基礎的なアプローチを採っている。
  論文  参考訳（メタデータ） (2024-05-03T14:52:47Z)
• Sequencer Level Security [2.756899615600916]
  本稿では,ロールアップのシークエンシングプロトコルであるSequencer Level Security (SLS)プロトコルを紹介する。 本稿では、ロールアップメムプールに送信されたトランザクションと、レイヤ1から派生したトランザクションの両方に対するプロトコルの仕組みについて述べる。 我々は,GethとOPスタック上に構築されたSLSプロトコルであるZircuitのプロトタイプを実装した。
  論文  参考訳（メタデータ） (2024-05-03T02:47:40Z)
• Trustless Audits without Revealing Data or Models [49.23322187919369]
  モデルプロバイダが(アーキテクチャではなく)モデルウェイトとデータシークレットを維持しながら、他のパーティがモデルとデータプロパティを信頼性のない監査を行うことが可能であることを示す。 私たちはZkAuditと呼ばれるプロトコルを設計し、モデルプロバイダがデータセットとモデルの重みの暗号的コミットメントを公開します。
  論文  参考訳（メタデータ） (2024-04-06T04:43:06Z)
• Enhancing Trust and Privacy in Distributed Networks: A Comprehensive Survey on Blockchain-based Federated Learning [51.13534069758711]
  ブロックチェーンのような分散型アプローチは、複数のエンティティ間でコンセンサスメカニズムを実装することで、魅力的なソリューションを提供する。 フェデレートラーニング(FL)は、参加者がデータのプライバシを保護しながら、協力的にモデルをトレーニングすることを可能にする。 本稿では,ブロックチェーンのセキュリティ機能とFLのプライバシ保護モデルトレーニング機能の相乗効果について検討する。
  論文  参考訳（メタデータ） (2024-03-28T07:08:26Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  既存の機械学習ベースの脆弱性検出方法は制限され、スマートコントラクトが脆弱かどうかのみ検査される。 スマートコントラクトのための初のDeep Neural Network(DNN)ベースの脆弱性検出フレームワークであるESCORTを提案する。 ESCORTは6種類の脆弱性に対して平均95%のF1スコアを達成し,検出時間は契約あたり0.02秒であることを示す。
  論文  参考訳（メタデータ） (2021-03-23T15:04:44Z)

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

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