📄 Paper 01 · Systemization of Knowledge

SoK: Jamming Attacks and Defenses
on the Lightning Network

Ayelet Mizrahi (Kotzer), Aviv Zohar — Hebrew University of Jerusalem
AFT 2024 (Advances in Financial Technologies)
Lightning Network のチャネル Jamming 攻撃を初めて体系的に整理した SoK 論文。攻撃の分類・コスト定量化・既存防御策の統一評価フレームワークを提供し、「どの単一防御策も全攻撃形態を防げない」ことを証明。Upfront Fee + HTLC Endorsement の組み合わせを最有力な実装候補として提言した。
リサーチクエスチョン
RQ 1
Channel Jamming 攻撃はどのように分類でき、それぞれのコストはどの程度か？
RQ 2
提案されてきた防御策（Upfront Fee / Reputation / Endorsement / Circuit Breaker）はどの攻撃クラスに有効か？
RQ 3
単一の防御策で全攻撃形態を防ぐことは可能か？
RQ 4
現実的かつ実装可能な防御の組み合わせとして何が最適か？

なぜ Jamming は深刻な問題か

攻撃の根本的な非対称性

正常な支払いは成功すれば手数料を払う。しかし失敗する HTLC には手数料が不要（or ごくわずか）。攻撃者はほぼゼロコストでチャネルのスロットを埋め続けられる。

攻撃コストの実態

攻撃タイプ推定月間コスト
Slow Slot Jamming〜$10/月
Fast Slot Jamming数十〜数百ドル
Amount Jammingチャネル残高相当
研究の手順
1
攻撃の分類軸設計（2-Axis Taxonomy）
既存の jamming 攻撃を ①時間軸（Quick vs. Slow）× ②資源軸（Slot vs. Amount）の2次元で分類。4象限マトリクスを構築し、各クラスの定義を明確化する。
分類・体系化
2
攻撃コストの形式モデル構築
攻撃者の能力（送信元制御・タイムロック最大化・MPP 展開）を形式化。Opportunity cost = locked 流動性 × 期間 × 代替収益 として定量化。実際の LN ネットワークデータを参照して $10/月の数値を導出。
形式モデル + 定量分析
3
防御策の統一評価フレームワーク設計
Upfront fees / Local reputation / HTLC endorsement / Circuit breaker を
① 有効性（攻撃コスト引き上げ量）
② 副作用（正常支払いへのオーバーヘッド）
③ 実装複雑性（BOLT 互換性）
④ 情報要件（グローバル vs. ローカル）
の4軸で評価できる共通フレームワークを設計する。
評価フレームワーク設計
4
各防御策の攻撃クラス別評価
4象限の各攻撃タイプに対して、各防御策がどの程度有効かをフレームワークで評価。Stake Certificates（UTXO backed reputation）も独立して分析。定性的評価 + コスト試算を組み合わせる。
比較評価
5
Layered Defense の必要性の論証と政策提言
単一防御策の不十分さを定量的に示した後、Upfront fees + HTLC endorsement の組み合わせが現実的な balanced approach であることを論証。BOLT への標準化必要性を明記し、実装コミュニティに具体的な政策提言を行う。
政策提言

攻撃の 4 象限マトリクス

Quick（短時間・高頻度）Slow（長時間・低頻度）
Slot Jamming高コスト・発見しやすい⚠ 最安・最危険（月$10〜）
Amount Jamming中〜高コスト中コスト（残高相当の資本が必要）
主要結果
4
攻撃クラス
（2軸分類）
~$10
Slow Slot Jamming
の月間コスト
0
全攻撃を単独で
防げる防御策
483
HTLC スロット上限
（攻撃の根源）
防御策比較（評価結果）
防御策Quick JammingSlow Jamming副作用実装難度
Upfront fees（無条件）高高全 HTLC に fee 追加中
Upfront fees（条件付き）中中低高
Local Reputation低中低中
HTLC Endorsement中中低中
Circuit Breaker中低 ⚠低低
💡 最有力な組み合わせ: Upfront Fees + HTLC Endorsement。Slow Jamming への唯一有効な防御（upfront fee）と、Sybil 対策（reputation）を補完的に組み合わせる。lnd などが endorsement フラグのプロトタイプを実装中。
課題と限界
📐
攻撃コストモデルの単純化
$10/月の試算は stylized model。実際の LN グラフのトポロジー・fee 分布・チャネル利用率は考慮が不十分。実際のコストは大きく異なる可能性がある。
🔍
Reputation の実証不足
Local reputation の有効性は実際の LN ノードデータで検証されていない。新規ノードが Sybil 攻撃を仕掛けた場合の動態が理論のみで評価されている。
🔀
MPP との相互作用
Multi-Path Payment が jamming 攻撃・防御双方に与える複雑な影響が簡略化されている。攻撃者が MPP を悪用して複数チャネルを同時に攻撃するシナリオの評価が薄い。
⚖️
ゲーム理論的均衡の欠如
fee 引き上げ後に攻撃者・防御者がどう戦略を変化させるかの動的均衡分析（Nash / Stackelberg）がない。防御導入後のシステム変化が未評価。
📋
BOLT 標準化の具体案が未定
「BOLT への標準化が必要」という政策提言はあるが、具体的な BOLT 変更案の詳細は将来課題として残す。実装者が参照できる仕様レベルの提案がない。
⚡ 未解決問題: Slow Slot Jamming への根本解は「fee なし HTLC を許可する現行設計の変更」以外にない。これは HTLC のインセンティブ設計全体に関わる未解決問題として明示されている。
📄 Paper 02 · Privacy / Machine Learning

Channel Balance Interpolation
in the Lightning Network via Machine Learning

Vincent Davis, Emanuele Rossi, Vikash Singh — Amboss Technologies; VantAI; Stillmark
arXiv 2024
能動的な probing（試験 HTLC 送信）を一切使わず、公開情報とグラフ構造だけからチャネル残高を推定する Random Forest モデルを提案。Laplacian positional encoding（グラフ位置情報）が最重要特徴量（MDI 33.3%）と判明。Equal-split ベースラインより 27.6% 低い誤差を達成し、既存の Differential Privacy 防御が通用しない新世代のパッシブ攻撃を実証した。
リサーチクエスチョン
RQ 1
試験 HTLC を送信しないパッシブな観察だけで、チャネル残高比率を予測できるか？
RQ 2
グラフ構造（トポロジー）情報と経済情報（fee / capacity）ではどちらが予測に有効か？
RQ 3
既存の能動 probing 防御（Differential Privacy）はこのパッシブ ML 推定に対しても有効か？
RQ 4
残高の「どちら側が多いか」という方向性の予測精度はどの程度か？

なぜパッシブ ML 推定が革命的なのか

従来の攻撃（能動 probing）

故意に失敗する HTLC を送って残高の上下界を絞る二分探索。痕跡が残る・コストがかかる・DP 防御が有効。

本手法（パッシブ ML）

Gossip データ + グラフ構造だけ。痕跡なし・コストゼロ・既存防御が効かない。根本的に異なる攻撃面。

研究の手順
1
問題の定式化：残高比率の予測問題として捉え直す
チャネル残高を p_{u,v} = y_{u,v} / c_{u,v} ∈ [0,1] という比率で定義。容量 c_{u,v} は公開情報だが、各方向の残高 y_{u,v} は非公開。これを予測する回帰問題として定式化。保存則 p_{u,v} + p_{v,u} = 1 を制約として明示する。
問題設定
2
特徴量の設計（3グループ）
① ノード特徴量: Feature flags（wumbo flag 等）、Capacity Centrality（ノードの容量 ÷ ネットワーク合計）、Fee Ratio
② エッジ特徴量: Time Lock Delta、Min/Max HTLC、Fee Rate (ppm)、Fee Base
③ Positional Encoding（鍵）: グラフ Laplacian の固有ベクトル。ノードの「グラフ上の位置」を数値化。約1秒で計算可能。
特徴量エンジニアリング
3
データセット収集（Amboss クラウドソース）
2023年12月15日時点の LN スナップショット（約7,500ノード・40,000エッジ）。真の残高データは Amboss Technologies のノードオペレーターが自発的に共有したもの（オプトイン）を使用。80/10/10% で train/valid/test 分割。
データ収集
4
6種類のモデル構成を比較実験
Equal Split（p̂=0.5）・Local Max HTLC をベースラインとして、
Nodes only / Edges only / Concatenated / Shallow（PE only）/ Joint（全結合）
の6種を Random Forest で実装・評価。MAE_p（比率誤差）と R²（決定係数）で比較。
アブレーション実験
5
Feature Importance 分析で支配要因を特定
MDI（Mean Decrease in Impurity）で各特徴量の貢献度を測定。Positional Encoding が MDI 33.3% で断トツ1位と判明。これは「ネットワーク上の位置がチャネル残高分布と強く相関する」という重要な示唆を与える。
解釈性分析
主要結果
-27.6%
Equal Split 比
の MAE_p 削減
33.3%
Positional Encoding
の MDI 重要度
0.74
残高方向判別
Precision
R²=0.365
Joint モデル
の決定係数
モデル性能比較
モデルMAE_p ↓R² ↑改善率
Equal Split（baseline）0.358-0.001—
Nodes Only0.3130.097-12.6%
Edges Only0.3160.115-11.7%
Shallow (PE only)0.2850.275-20.4%
Concatenated0.2650.351-26.0%
Joint (best)0.2590.365-27.6% ★
💡 重要な示唆: Positional Encoding の圧倒的な重要度（33.3%）は、LN のスケールフリー構造（hub-spoke）が残高分布と強相関していることを示す。ハブノードに繋がるチャネルの残高はハブ側に偏る傾向があり、これが ML に大きなシグナルを与える。
課題と限界
📉
R² = 0.365 — 説明力は 36.5% のみ
残高変動の 63.5% は未説明。個別チャネル残高の正確な推定は構造的に困難。「どちら側が多いか」という方向判別（precision 0.74）が現実的な精度上限である可能性。
📊
データバイアス：Amboss オプトインノードに偏る
真の残高データはオプトイン参加者のみ。大口ルーティングノードに偏り、一般的なノードを代表していない可能性がある。
⏱
時系列変動の未考慮
スナップショット1枚のみで学習。残高は動的に変化するため、モデルの有効期限・再学習頻度が実用上の問題になる。
🛡
防御策との非対称性
Twilight（DP ノイズ）等の既存防御は能動 probing を対象に設計。本手法（パッシブ ML）には効果がほぼない。新たな防御（fee policy の差分プライバシー化・グラフ構造難読化）が必要。
📄 Paper 03 · Game Theory / Security

Securing Lightning Channels
against Rational Miners

Lukas Aumayr, Zeta Avarikioti, Matteo Maffei, Subhra Mazumdar — TU Wien; Common Prefix; IIT Indore
ACM CCS 2024
Lightning チャネルの安全性が「マイナーが正直である」という暗黙の前提に依存していることを Extensive-Form Game（EFG） で初めて formal に証明。Byzantine 攻撃者 + rational miner の組み合わせでは既存設計が崩れることを示し、CRAB（Channel Resistant Against Bribery）という担保ベースのチャネル設計と、オフライン対応の Sleepy CRAB を提案した。
リサーチクエスチョン
RQ 1
Rational（手数料最大化）マイナーを仮定したとき、Lightning チャネルの Penalty 機構は安全か？
RQ 2
Byzantine 攻撃者がマイナーを買収した場合、既存の Lightning Channel は fund safety を保てるか？
RQ 3
Rational Miner に対して fund safety を保証するチャネル設計は可能か？
RQ 4
チャネル当事者がオフラインになる場合にも、Rational Miner に対して安全なチャネルを設計できるか？

攻撃の仕組み：Timelock Bribing

攻撃者 A が古い状態を Broadcast:
  A ──publishes──► txA,0 (古い状態, A が全額 v を保有)
  B ──publishes──► revocation TX (fee = f_b)
  A ──bribes  ──► miners (fee = f_a, ここで f_a > f_b)
  Miner ──accepts► A's tx, ignores B's tx → A が勝つ

→ A は最大 v（チャネル全額）を bribe として提供できる
研究の手順
1
問題の定式化：3プレイヤー Extensive-Form Game
Lightning Channel の close フェーズを A（攻撃者）・B（被害者）・M（マイナー） の3プレイヤーゲームとして定式化。各プレイヤーの action sequence とペイオフ関数を設計する。Subgame Perfect Nash Equilibrium（SPNE）を backward induction で導出する手法を選択。
ゲーム理論的定式化
2
既存の Lightning Channel（LC）の安全性分析
Theorem 1: Rational party + Rational miner の組み合わせでは、双方がメンプールを常時監視する条件下で LC は安全（SPNE）。
Corollary 2: Byzantine party + Rational miner の組み合わせでは LC は本質的に安全でない。Byzantine A は損失を厭わないため、v+δ の bribe を提示できてしまう。
既存設計の安全性証明
3
CRAB の設計：インセンティブを逆転させる
核心アイデア: Revocation TX を mine するとマイナーが v + c を得られるようにする（c = 担保）。攻撃者が提供できる最大 bribe は v（チャネル残高）のみ。
v + c > v → Rational miner は常に revocation を選ぶ → 攻撃が経済的に無意味になる。
c = v/2 で十分なことを Section 4.3 で証明。
プロトコル設計
4
Sleepy CRAB：オフライン対応への拡張
CRAB でも B がオフラインだと A の old state 投稿に即応できない問題を解決。タイムロック付き担保により、Miner 自体が罰則 TX を取るインセンティブを持つ設計に拡張。これにより当事者がオフラインでも Rational Miner が自発的に不正を阻止する。
拡張設計
5
Proof-of-Concept 実装と比較評価
Bitcoin Script（DS + CSV のみ）で CRAB/Sleepy CRAB を実装。Turing-complete 不要。追加担保・TX 数・通信コストを表で整理し、DMC / LC / Sleepy / Brick / Cerberus と系統的に比較。
実装 + 比較
主要結果
v/2
CRAB に必要な
最小担保額
初
Byzantine + Rational
Miner + Offline 対応
SPNE
証明の手法
（均衡分析）
0
Turing-complete
スクリプト要件
既存設計との比較（Table 1）
設計Byzantine 攻撃者Rational MinerOffline 対応Permissionless
Lightning Channel (LC)✗△✗✓
Sleepy Channels✗✗✓✓
Cerberus✗✗✓✓
CRAB（本論文）✓✓✗✓
Sleepy CRAB（本論文）✓✓✓✓ ★
💡 Lightning の暗黙の前提を暴いた: これまで「Honest Miner」として片付けてきた前提が、channel fund safety を担保していた。Sleepy CRAB はこの前提を取り除いた初の設計で、Bitcoin Script のみで実現できる。
課題と限界
💰
担保コスト：2v が高い
CRAB は両者合計で 2v の担保が必要（既存 LC の 2δ より大幅に高い）。資本効率が低下し、ルーティングノードにとって経済的な負担になる。
👁
メンプール監視の楽観的前提
Theorem 1 は「Rational party が常時メンプールを監視する」を前提とする。現実のノードは必ずしも 24/7 監視しないため、前提条件の実現可能性が問題。
🔗
マルチホップ・HTLC への未適用
分析は 2-party channel に限定。HTLC chain を通じたマルチホップでの bribing（中間ノードが miner を買収）は別問題として未解決。
⛏
マイナーの分散化前提
≥2 の競合マイナーが存在することが tight analysis の前提。マイニングプールの高度な中央集権化（top 5 pool が 80%+ のハッシュレート）でこの前提が崩れる可能性。
📄 Paper 04 · Mathematical Theory

A Mathematical Theory of
Payment Channel Networks

Rene Pickhardt — Independent / Blockstream Research
arXiv 2026
PCN の送金可能性・スループット・Channel Depletion を 多面体幾何学（polytope geometry） として統一的に形式化した理論論文。チャネルの流動性状態集合が m 次元整数ハイパーボックスと同型であることを証明し、Throughput Law S = ζ/ρ を導出。Lightning が Visa 規模のスループットを達成するには Multi-Party Channel が数学的必須 であることを厳密に示した。
リサーチクエスチョン
RQ 1
PCN の「送金可能性（feasibility）」は、チャネルの実際の残高配置ではなく何に依存するか？
RQ 2
PCN のオフチェーンスループットはどのような数学的法則で上界されるか？
RQ 3
Multi-Party Channel（coinpool / channel factory）は資本効率をどの程度改善するか？
RQ 4
Channel Depletion は現行の fee 設計の下で数学的に不可避か？どう防ぐか？

なぜ幾何学で PCN を捉えるのか

「残高が偏る（Depletion）」「大口送金が失敗する（Infeasibility）」という現象の原因について、従来の説明は矛盾していた。幾何学的フレームワークはこれらを 高次元ポリトープの射影 として統一的に説明する。

流動性状態 LG ≅ m次元整数ハイパーボックス（チャネルごとに1自由度）
資産分布 WG = LG の射影（n次元空間への写像）
→ WG は必ずW(C,n)の真の部分集合
→ 必ず「実現不可能な資産分布」が存在する
研究の手順
1
流動性状態の多面体 LG を定義・証明
LG = 全実現可能流動性関数の集合 を定義。Lemma 3.2: LG は m 次元整数ハイパーボックスと同型 LG ≅ {0,...,c1} × ... × {0,...,cm} を証明。各チャネルの残高が1つの独立した自由度を持つため、m チャネルで m 次元ボックスになる。
数学的定義・補題証明
2
資産分布の多面体 WG と送金可能性の形式化
WG = LG を「ユーザーごとの残高合計」に射影した集合。Lemma 4.2: n>2 では WG は W(C,n) の真の部分集合 → 実現不可能な資産分布が必ず存在。
送金の feasibility 判定: 送金後の資産分布 w' が WG に留まるかどうかに帰着（実際の残高配置 λ ではなく資産分布 ω だけに依存）。
送金可能性の幾何的特徴付け
3
Throughput Law の導出
S = ζ / ρ（オフチェーン TPS = オンチェーン TPS ÷ 期待不可能送金率）を導出。
Bitcoin の ζ = 7 TPS 固定、Visa 並み S = 47,000 TPS に必要な ρ < 0.015%。
2-party channel の実測 ρ はこれより大幅に高い → 2-party PCN は幾何学的にスケールしない。
スループット法則の導出
4
Multi-Party Channel の資本効率を解析的に評価
k-party channel を k-uniform hyperedge としてモデル化。Lemma 5.1（Cut interval lemma）: 全カットの期待幅が k に比例して線形拡大 → WG が単調増加。1ノードの期待 accessible wealth が k/n に比例 → k が大きいほど capital efficiency が線形改善。
Multi-Party Channel の解析
5
Channel Depletion の数学的証明と緩和策の提示
線形非対称 fee 関数（一方向にだけ手数料がかかる）下では、コスト最小化フローが WG の境界に向かう循環を作ることを証明。Generic に全チャネルが depleted になる。
3つの緩和策: ①対称 fee ②凸/tier 手数料 ③協調 replenishment。
証明 + 設計提言
主要結果
S=ζ/ρ
Throughput Law
（オフチェーン TPS）
<0.015%
Visa 達成に必要
な ρ（不可能率）
k/n
k-party channel の
資本効率改善
m次元
流動性状態空間の
幾何的次元
主要定理・補題一覧
定理 / 補題内容意義
Lemma 3.2LG ≅ m次元整数ハイパーボックス流動性状態空間の完全な幾何的表現
Lemma 4.2WG ⊊ W(C,n)（n>2）PCN には必ず実現不可能な資産分布が存在
Theorem（Throughput）S = ζ/ρオフチェーンスループットの数学的上限
Lemma 5.1k-party channel → WG 単調拡大Multi-party channel が capital efficiency を線形改善
Depletion Theorem線形非対称fee → 全チャネルが depletedChannel Depletion の数学的必然性を証明
⚡ 実務への最大の示唆: 2-party PCN は数学的にスケールしない。Multi-party channel（coinpool / channel factory）が唯一の根本解だが、Bitcoin の ANYPREVOUT（BIP-118）が必要で現時点では未採用。
課題と限界
🧮
Feasibility 判定は NP 困難の場合あり
WG に点が属するかの判定は整数線形計画（ILP）に帰着するため、大規模ネットワークでの実時間適用が困難。近似アルゴリズムの開発が必要。
📐
基本モデルは fee・メタデータを除外
セクション1で明示されているように、fee・オンチェーン手数料・ルーティングポリシーを除いた単純化モデルが出発点。実際の LN への適用には追加の仮定が必要。
🔧
Multi-Party Channel の実装に ANYPREVOUT が必要
理論的に最も重要な解（k-party channel）の実装には BIP-118 が必要だが、Bitcoin のコンセンサス変更は未定。実装可能時期が不明確。
📝
証明の機械検証なし
定理の証明は手書き（Proof assistant 不使用）。Why3 / Coq による機械検証は対象外。Fabiański (FC 2025) との対比が際立つ。
📄 Paper 05 · Formal Verification

A Formally Verified
Lightning Network

Grzegorz Fabiański, Rafał Stefański, Orfeas Stefanos Thyfronitis Litos — University of Warsaw; Imperial College London
FC 2025 (Financial Cryptography)
Why3 証明アシスタントを使って Lightning Network の 2-party channel を WhyML で実装し、Byzantine 相手方が存在するあらゆるシナリオで honest user の資金安全性（Funds Security）が成立することを機械検証可能な形で初めて証明した。6,060 行のプログラムコード + 7,420 行の証明コードからなる。無制限（non-PPT）敵に対しても有効な unconditional な保証を提供する。
リサーチクエスチョン
RQ 1
Lightning Network の fund safety を機械が検証できる（machine-checkable）形で証明できるか？
RQ 2
Byzantine 相手方 + 無制限敵（non-PPT）に対しても、honest user の資金は常に保護されるか？
RQ 3
計算論的仮定（PPT adversary・暗号の強さ）に依存せずに fund safety を証明できるか？
RQ 4
lnd / CLN のような production 実装の fund safety を証明するための blueprint を提供できるか？

なぜ機械検証か — 手書き証明の限界

従来アプローチ（Litos-Zindros 2020）

UC（Universal Composability）フレームワークで LN をモデル化。ただし UC ペーパープルーフは人間が書いた証明 → 見落としのリスクが残る。

本論文のアプローチ

Why3 + SMT solver（Alt-Ergo, CVC4）でコンピュータが全証明パスを検証。digital signature を理想機能として抽象化 → PPT 前提不要でより強い保証。

研究の手順
1
Bitcoin サブセットモデル（Γ）の WhyML 実装
LN に必要な Bitcoin 機能だけをサブセット化: UTXO モデル（txid / Input / Output / TimeLock / Witness）、絶対タイムロック（CLTV）、相対タイムロック（CSV）。デジタル署名は GMR 理想機能として抽象化（signaturesFunctionality.mlw）。
モデル設計・実装
2
Funds Security の形式定義
1-player game として形式化: 敵が 6 種類のアクション（SignMsg / SendMsgToGamma / DeliverMsgToGamma / IncrementTime / SendMsgToParty / ControlEnvironment）を任意の順序で実行。
Funds Security: 「honest party が close を要求すれば、有界時間 T 以内に正当残高を受け取る」。
安全性定義の形式化
3
2段階 Modular Proof 設計
Stage 1: LN 実装が requirements を満たすことを Why3 で証明（honestPartyInterface.mlw）。
Stage 2: requirements を満たす任意実装が fund safety を享受することを証明。
→ Stage 2 は Blueprint: lnd/CLN も同 requirements を満たすと別途示せば fund safety が得られる。
モジュラー証明設計
4
Evaluator 抽象化の設計
「誰がいくら持っているか」の形式定義が LN では自明でない問題を解決。Evaluator モジュールを設計: off-chain 署名済みの commitment TX も含めた資産所有権の「唯一の真実」として機能する抽象化。他の verification プロジェクトでの再利用を想定。
抽象化設計
5
SMT Solver による全証明の機械検証
Alt-Ergo + CVC4 SMT solver で 7,420 行の証明コード（lemmas / assertions / postconditions）を全て機械検証。証明構築過程で HTLC timeout の境界条件に関する corner case を 2 件発見（仕様のバグ可能性を指摘）。
機械検証・バグ発見
主要結果
初
LN fund safety の
machine-checkable 証明
6,060
プログラムコード
（行数、WhyML）
7,420
証明コード
（行数）
2件
発見されたコーナー
ケース（仕様バグ）
Why3 vs TLA+ — 2つの形式検証アプローチの比較
観点Fabiański (Why3, 本論文)Grundmann (TLA+)
アプローチ定理証明（SMT solver）モデル検査（状態空間探索）
強みUnconditional proof
機械検証・無限パスに対応		自動反例探索
Multi-hop 対応
弱み2-party のみ
HTLC 非対応		有限状態空間の coverage に限る
対象Fund safety（2-party, HTLC なし）Multi-hop security
敵モデルUnbounded（非 PPT）通常モデル
💡 Blueprint の価値: Stage 2 の証明は production 実装への橋渡し。lnd / CLN が honestPartyInterface.mlw の requirements を満たすことを別途示せば、それらの fund safety も guarantee できる。実用的な検証パスを初めて提示した。
課題と限界
🔗
マルチホップ・HTLC が対象外
最も重要なユースケース（HTLC を使ったマルチホップ送金）が証明対象外。$120M 超の資産の大半はこの経路で動く。Litos-Zindros の UC モデルは存在するが machine-checkable ではない。
💸
オンチェーン手数料が考慮されない
fee griefing / CPFP / RBF などのオンチェーン dynamics は対象外。Fund safety の証明が成立しても、force close 時の手数料で資産が実質的に失われるシナリオは未評価。
⏸
Liveness（生存性）が未証明
双方向同時支払いでデッドロックが発生する可能性が残る。Fund safety（資金は失われない）は証明されても、「支払いが完了する」という liveness は保証されていない。
📏
Full BOLT 仕様との Gap
本実装は BOLT の "simplification"。BOLT 1-12 全体の機械検証は未達成。実際の lnd / CLN 実装との仕様 gap が残る可能性がある。
💡 2025 年の転換点: 本論文（Why3）と Grundmann (TLA+) の独立並走は、formal verification コミュニティが Lightning に本格参入した転換点。HTLC + マルチホップの machine-checkable 証明が次の frontier。
📄 Paper 06 · Privacy / Cryptography

Anonymous Multi-Hop Locks for
Blockchain Scalability & Interoperability

Giulio Malavolta, Pedro Moreno-Sanchez, Clara Schneidewind, Aniket Kate, Matteo Maffei
NDSS 2019
HTLCに潜むWormhole攻撃を初めて形式化——中間ノードが共謀して手数料を横取りする攻撃がHTLCでは原理的に防げないことを証明。対策としてAnonymous Multi-Hop Locks（AMHL）とAdaptor Signature ベースのPoint Locks（AS-PoP）を提案。Bitcoin互換かつ匿名性・原子性を同時に達成し、PTLCの理論的礎を築いた。
リサーチクエスチョン
RQ 1
既存のHTLCベースPCNはWormhole攻撃を原理的に防ぐことができるか？
RQ 2
原子性を保ちながら送受信者の関係匿名性を強化できるロック機構は設計可能か？
RQ 3
secp256k1（Bitcoin）でも動作する実用的なAMHL実装は可能か？
RQ 4
クロスチェーンPCN（Bitcoin×Ethereum等）にAMHLはどう適用できるか？

Wormhole攻撃——HTLCの構造的欠陥

攻撃の仕組み

A→B→C→D→E という経路でAがEに支払う際、BとDが共謀して中間ノードCをスキップ。Cに向かうHTLCをBが先にDへ渡し、Cのルーティング手数料を横取りする。

HTLCの根本問題

HTLCは同一ハッシュpreimageをパス全体で共有。共謀ノードが先読みしてpreimageを取得できるため、防御は原理的に不可能。

研究の手順
1
Wormhole攻撃の形式化・HTLCの脆弱性証明
PCNのセキュリティモデルを整備し、Wormhole攻撃を形式的に定義。共謀ノードペアが中間経路をバイパスして手数料横取りできることをゲーム理論的に証明。HTLCがこの攻撃に本質的に脆弱であることを示す。
攻撃の形式化
2
AHMLの抽象プリミティブ設計（3要件の定式化）
①Wormhole防止・②関係匿名性・③原子性の3要件を形式化。AMHLという抽象プリミティブを定義し、理想的な性質を記述。HTLCがこれを満たさないことを証明する。
セキュリティ定義
3
AS-PoPの設計——Adaptor Signatureによる実装
各ホップでランダムスカラーを加算するPoint Locks（AS-PoP）を設計。隣接ノードがpreimageを逆算できないよう経路ごとに独立化。secp256k1上のBitcoin互換実装を提示。
プロトコル設計
4
セキュリティ証明（EUF-CMA前提）
AS-PoPがAMHLの全3要件を満たすことを形式証明。EUF-CMA安全な署名スキームを前提として関係匿名性とWormhole耐性を同時に達成することを示す。
形式証明
5
クロスチェーン拡張（Bitcoin×Ethereum）
EthereumのECDSAとBitcoinのSchnorrが混在するクロスチェーン送金でも同一フレームワークが適用可能であることを示す。PCN相互運用性の理論基盤を提供。
拡張・応用
主要結果
初
Wormhole攻撃の
形式的証明
3
同時達成の性質
（Wormhole耐性・匿名性・原子性）
~400B
追加オーバーヘッド
（per hop vs HTLC）
PTLC
BTCへの採用路線
（Taproot + Schnorr）
性質HTLCAMHL (AS-PoP)
Wormhole耐性✗ 本質的に脆弱✓ 形式証明済み
関係匿名性✗ 同一ハッシュで特定可✓ ホップごとに独立
原子性✓✓
Bitcoin現時点互換✓△ Taproot後
課題と限界
⛓️
TaprootとSchnorrが必要
AS-PoPはSchnorr署名とTaprootが前提。2021年にActivateされたが、LightningのTaproot Channel移行は現在も進行中。
🔍
残高プロービング攻撃は別問題
AMHLはWormholeと関係匿名性を防ぐが、残高probing攻撃には効果なし。Twilight（DP）のような直交した防御が別途必要。
🌐
全ホップのアップグレードが前提
経路上の1ホップでもHTLCが混在すると、そのホップからWormhole攻撃が成立する。移行期間中の保証が難しい。
📐
完全な送受信者匿名化は非対象
関係匿名性（同一経路のペアを特定できない）は達成するが、送信者・受信者の完全匿名化は別の問題（onion routingと組み合わせて対処）。
📄 Paper 07 · Security / On-chain Attack

Flood & Loot: A Systemic Attack
on the Lightning Network

Jona Harris, Aviv Zohar — Hebrew University of Jerusalem
AFT 2020 (Advances in Financial Technologies)
多数のチャネルを同時に強制クローズさせてブロックチェーンを輻輳状態に追い込み、HTLCのタイムロック切れを悪用して支払いを盗むシステミック攻撃を初めて提示。わずか85チャネルを同時攻撃することで収益性が成立し、Bitcoin低スループット（7 TPS）が根本的脆弱性であることを示した。
リサーチクエスチョン
RQ 1
多数チャネルを同時強制クローズさせることでHTLCを盗む攻撃は成立するか？
RQ 2
攻撃が収益性を持つために必要な最小チャネル数はどの程度か？
RQ 3
Bitcoin低スループットとRBF非対称性はどのように攻撃を増幅させるか？
RQ 4
Anchor Outputsや長タイムロック等の対策は攻撃を無効化できるか？

攻撃の2ステップ

Step 1: Flood（洪水）

攻撃者が同時に多数のHTLC付きチャネルを強制クローズ。on-chainに大量のTXを送り込んでmempool輻輳を作り出す。

Step 2: Loot（略奪）

HTLCタイムロック切れ前に被害者が防御TXを確認させられない。タイムロック後に攻撃者がHTLC resourceを回収（preimageなしで）。

研究の手順
1
攻撃シナリオの形式化
マルチホップHTLCにおけるタイムロック競合を形式化。攻撃者が複数経路にまたがるHTLCを同時に保留し、期限切れ後に回収する「並列強制クローズ」のモデルを構築。
攻撃モデル
2
Bitcoin スループットとRBF非対称性の分析
Bitcoin7 TPS vs 被害者の防御TX量を計算。RBF（Replace-By-Fee）の非対称性——攻撃者は複数TX一括でfeeを上げられるが被害者は個別に高コスト——を定量化。輻輳下での防御困難さを示す。
オンチェーン分析
3
収益性の閾値計算
攻撃コスト（チャネル開設fee + on-chain fee）と収益（盗めるHTLC量）を比較。N = 85チャネルが損益分岐点であることを数値的に導出。チャネル容量と平均HTLC額を実データから推定。
コスト分析
4
対策の有効性評価
①タイムロック延長・②Anchor Outputs（CPFP対応）・③チャネル容量制限・④HTLCの段階的resolution のそれぞれについて、攻撃コストへの影響を分析。完全な解決策がないことを示す。
対策評価
主要結果
85
損益分岐チャネル数
（この数以上で収益）
7 TPS
Bitcoin根本スループット
（攻撃の源泉）
非対称
RBFコスト構造
（攻撃者有利）
初
システミックLN攻撃の
定量分析
⚠️ Anchor Outputs（BOLT 3 / BOLT 5 更新）は本攻撃を部分的に緩和。被害者がCPFPで防御TXのfeeを引き上げやすくなったが、mempool輻輳が激しい場合は依然として攻撃成立の可能性がある。
対策効果限界
タイムロック延長攻撃コスト増加資本効率低下
Anchor Outputs (CPFP)被害者が反撃しやすい極端な輻輳では不十分
HTLC数制限被害上限を下げるルーティング容量も低下
課題と限界
💰
初期資本が必要
85チャネル以上を開設するための on-chain TX費用と担保資本が必要。低fee環境では安くなるが、攻撃実行時はfeeが高騰するため実際のコストは変動する。
🔗
Bitcoinスループットは根本解決不可
7 TPSの制約はBitcoinのコンセンサスパラメータに起因。Lightning側の対策だけでは完全解決できない構造的問題。
📡
実際のmempool観測が困難
攻撃者がmempool状況をリアルタイムに把握・制御する必要がある。輻輳の作り出し方と被害者の反応を事前に予測するのが難しい。
📄 Paper 08 · Privacy / Attack

Probing Channel Balances in the
Lightning Network

Sergei Tikhomirov, Romanus Nowostawski, Jan Mattsson — Simula Research Lab / UC Riverside
FC 2020 (Financial Cryptography)
HTLCのエラーメッセージの違いを悪用した二分探索プロービングにより、1 satoshi精度でチャネル残高を推定できることを実証。失敗したHTLCには手数料がかかない構造的欠陥により攻撃コストがほぼゼロ。エラー種別の分析から「worst of both worlds」——残高も分かり、エラー統一化も使いにくい——という診断を下した。
リサーチクエスチョン
RQ 1
攻撃者は実際の送金なしにチャネル残高を精密に推定できるか？
RQ 2
どのHTLCエラーコードが最も多くの残高情報を漏洩させるか？
RQ 3
プロービング攻撃の実際のコストと実行時間はどの程度か？
RQ 4
エラーコードの統一化は有効な防御策になるか？何が失われるか？

「Worst of Both Worlds」診断

現状の問題

HTLC失敗は無料。攻撃者は繰り返し試せる。エラー種別（unknown_next_peer vs temporary_channel_failure）が残高情報を開示する。

防御の딜레마

エラーを統一すれば（unknown_failure）残高は隠せるが、送金者・開発者がデバッグできなくなる。どちらも選べない「板挟み」状態。

研究の手順
1
BOLT仕様のHTLCエラーコード分析
BOLT 4のonionエラーメッセージ仕様を精査。残高不足・ノード到達不能・ルート不明などの異なるエラーコードが「どのポイントでなぜ失敗したか」を漏洩することを確認。
仕様分析
2
二分探索プロービングアルゴリズムの設計
チャネル容量を上限とし、HTLC金額を二分探索で絞り込む。temporary_channel_failure（残高不足）と成功の境界を検出することで1 sat精度を達成。~30回のプローブで完了。
アルゴリズム設計
3
テストネット実装・検証
テストネット環境にLightningノードを展開しアルゴリズムを実装。攻撃の実行時間・コスト・精度を測定。自分たちのチャネルで正解値と比較してバリデーション。
実装・検証
4
mainnetでの倫理的評価
実際のmainnetチャネルに対して限定的にプロービングを実施（倫理ガイドラインに従い）。エラーコードのばらつきとノード実装の差を観察。大規模実行の可能性を定量的に見積もる。
実証評価
5
対策の評価とトレードオフ分析
エラー統一化・レートリミット・PTLCへの移行・残高ランダム化の各対策を評価。いずれも完全な解決策でないことを示し「worst of both worlds」という診断を下す。
対策分析
主要結果
1 sat
達成可能な
残高推定精度
~30
1チャネルに必要な
プローブ回数
≈ 0
攻撃コスト
（失敗HTLCは無料）
数時間
mainnet全チャネル
プロファイリング時間推定
情報漏洩エラーコード一覧
エラーコード意味漏洩情報
temporary_channel_failure残高不足正確な残高境界
unknown_next_peerノード到達不能トポロジー情報
fee_insufficient手数料不足fee policy
permanent_channel_failureチャネル閉鎖少（閉鎖の事実のみ）
課題と限界
⚖️
防御と診断のトレードオフ
エラーを統一化すれば残高は隠せるが、正当な送金者・開発者のデバッグ能力が失われる。Lightning Networkの可用性と残高プライバシーは本質的にトレードオフ関係にある。
🔄
PTLCへの移行で一部緩和のみ
PTLCはpreimage相関をなくすが、HTLC同様に失敗プロービングでのエラーコード漏洩は発生する。根本的な解決にはならない。
🕵️
Blinded Paths後の評価が必要
BOLT 12のBlinded Pathsは受信者のプライバシーを強化するが、中間ノードの残高プロービングは依然可能。後続研究（Twilight/DP等）の必要性を示す。
📄 Paper 09 · Model Checking / Protocol Security

Payout Races and Congested Channels:
Model Checking LN

Ben Weintraub, Cristina Nita-Rotaru, Rainer Böhme — Northeastern / University of Innsbruck
CCS 2024 (ACM Conference on Computer and Communications Security)
SpinモデルチェッカーとPromela言語でHTLCコミットメントプロトコルを有限状態機械（FSM）として形式化。状態空間探索によりHTLCコミットメントハンドシェイクに競合状態（race condition）が存在することを発見。主要LN実装（lnd/CLN/LDK）に影響する脆弱性を協調開示し、プロトコル仕様修正につなげた。
リサーチクエスチョン
RQ 1
HTLCコミットメントプロトコルに競合状態は存在するか？手動レビューでは見落とされているか？
RQ 2
Spinモデルチェッカーを用いてLN仕様の網羅的な状態空間探索は可能か？
RQ 3
発見された競合状態はどのような条件下で資金損失につながりうるか？
RQ 4
モデル検査によるプロトコル検証アプローチは他のBOLT仕様にも適用可能か？

なぜモデル検査が必要だったか

人手レビューの限界

BOLT仕様はHTMLドキュメントで記述。状態機械の全遷移パスを人手で追うのは事実上不可能。並行する双方向通信のinterleaving空間は指数的に拡大する。

Spinの強み

Spinは状態空間を自動的に網羅的に探索し、デッドロック・assertion違反・競合状態を自動検出。LTL（線形時相論理）での性質を検証できる。

研究の手順
1
BOLT 2 コミットメント仕様のFSM化
BOLT 2のHTLCコミットメントプロトコル（commit_sig・revoke_and_ack・update_add_htlc等）を有限状態機械として形式化。双方向の非同期通信を含む複雑な状態遷移をPromela言語で記述。
形式モデル構築
2
検証性質の定義（LTL仕様）
「資金安全性（fund safety）」「デッドロックフリー」「プロトコル進行性（liveness）」をLTL式で記述。Spinが自動的に反例を探索できるようにsafety/liveness propertyを定義。
性質定義
3
Spinによる状態空間探索
Spinを用いて全状態遷移パスを網羅的に探索。状態爆発を抑制するため部分順序削減（partial order reduction）とビットステートハッシュを組み合わせ。
モデル検査
4
競合状態の発見・反例の解析
Spinが生成した反例トレースを解析し、HTLCコミットメントハンドシェイクの特定シーケンスで両者が互いを「待ち続ける」デッドロック条件を発見。
バグ発見
5
協調開示・仕様修正
lnd・CLN・LDKの開発者に協調開示。BOLT仕様のambiguityを特定し、実装レベルの修正とBOLT仕様の明確化を提案。CCS 2024発表後にパッチが適用。
協調開示
主要結果
1件
発見された
HTLCコミット競合状態
3実装
影響を受けた
LN実装（lnd/CLN/LDK）
Spin
使用したモデルチェッカー
（Promela + LTL）
修正済
協調開示後の
パッチ適用状況
💡 Fabiański (Why3) との比較: 本研究（Spin）は状態空間の自動探索が強み。Fabiański (Why3) は任意の性質の機械証明が強み。Spin は有限状態で反例を見つけ、Why3 は無限パスへの一般的証明を行う。どちらもLN形式化の重要な柱。
課題と限界
💥
状態爆発問題
マルチホップシナリオ（3ホップ以上）や複数HTLC並行処理では状態数が指数的に増加し、現実的な時間での検証が困難。モデルは1チャネル・限られたHTLC数に絞る必要があった。
📋
BOLT仕様の一部のみ対象
BOLT 2のコミットメントプロトコルに絞った検証。BOLT 1（transport）・BOLT 4（onion）・BOLT 7（gossip）等は対象外。プロトコル全体の検証は未達成。
🔄
仕様変更への追従が必要
BOLTは継続的に更新される生きた仕様。Anchor Outputs・Taproot Channels等の大型変更のたびにモデルの再構築が必要で、継続的なメンテナンスコストがある。
📄 Paper 10 · Routing / Optimization

Optimally Reliable & Cheap
Payment Flows on Lightning

René Pickhardt, Stefan Richter
arXiv 2021 / Adopted by lnd, CLN, LDK
チャネル残高を一様分布でモデル化し、最小コストフロー（MCF）問題としてルーティングを定式化。MPPの成功確率を最大化しつつ手数料を最小化する最適なパス分割を求める。Dijkstra基準比で2倍以上の成功率を実現し、lnd・CLN・LDK各実装への採用につながった。
リサーチクエスチョン
RQ 1
チャネル残高の一様分布仮定はどの程度現実的か？経路成功確率の計算に使えるか？
RQ 2
MPPによる送金分割を最適化するフレームワークは設計可能か？
RQ 3
最小コストフロー（MCF）アルゴリズムはLightningルーティングに適用可能か？
RQ 4
既存のDijkstra/K-最短経路アルゴリズムと比べてどれだけ改善されるか？

なぜルーティングは難しいか

残高の不可視性

Lightning gossipはチャネルの容量は公開するが残高は非公開。どちらの方向にどれだけ流せるかが分からない状態でルーティングを決定しなければならない。

MPP分割の最適化

大きな送金を複数部分に分割して送る（MPP）場合、分割数・分割比・経路の組み合わせが指数的に存在。直感的な分割は最適でないことが多い。

研究の手順
1
残高分布モデルの選択（一様分布）
チャネル残高[0, capacity]の一様分布仮定を採用。送金額xの経路成功確率を P = (capacity - x) / capacity として定式化。実データとの照合でこの仮定が実用的に正確であることを検証。
確率モデル
2
MCF問題への変換
送金を「グラフ上のフロー最適化問題」として定式化。目標：経路成功確率の積を最大化 ≡ 対数コストの和を最小化。これが標準的なMCFとして解けることを示す。
最適化定式化
3
MCFアルゴリズムの適用
既存のMCFソルバー（COST-SCALING / SUCCESSIVE SHORTEST PATHs）を適用。コスト関数 c(e, f) = -log P(e, f) を各エッジに割り当て、フロー制約のもとで最小化。MPP部分決定も自動的に得られる。
アルゴリズム適用
4
シミュレーション評価（mainnetスナップショット）
LNグラフのmainnetスナップショットで各種送金額・ネットワーク状態をシミュレーション。Dijkstra・K最短経路・MCFの送金成功率と手数料を比較。
シミュレーション
5
実装への橋渡し（lnd/CLN/LDK）
実装コミュニティとの協力でMCFルーティングをlnd（「Mission Control」改善）・CLN（pay plugin）・LDK（probabilistic routing）へ組み込む提案。計算コストとルーティング品質のバランスを示す。
実装採用
主要結果
>2×
送金成功率の改善
（Dijkstra比）
MCF
アルゴリズムフレームワーク
（既存ソルバーを直接適用）
3実装
採用LN実装
（lnd / CLN / LDK）
一様
残高分布仮定
（実データで検証済み）
ルーティング手法成功率（大口送金）計算コストMPP最適性
Dijkstra（単一最短経路）低（〜50%）O(E log V)なし
K-最短経路中O(kE log V)部分的
Pickhardt MCF高（〜90%+）中（MCFソルバー）最適
課題と限界
⚡
計算コストとリアルタイム性
MCFソルバーはDijkstraより計算コストが高い。モバイルやリソース制約のあるノードでのリアルタイム支払いルーティングへの適用には実装上の工夫（キャッシュ・近似解）が必要。
📊
一様分布仮定の限界
チャネル残高は実際にはトランザクション履歴に依存し、一様分布からずれることがある。精度の高い残高推定（プロービングデータ等）を組み合わせれば改善できるが、プライバシーとのトレードオフが生じる。
🌐
ネットワーク全体の最適解は不可能
各ノードが局所情報のみで決定するため、ネットワーク全体の同時最適化はできない。複数送金者が同じチャネルを同時に使おうとすると干渉が生じる。
📄 Paper 11 · Virtual Channels / Protocol Design

Horcrux: Synthesize Fast and
Depletion-Resilient Virtual Channels

Tian Tian, Bing-Hong Liu, et al.
NDSS 2025 (Network and Distributed System Security)
仮想チャネルの残高枯渇（Depletion）攻撃を形式化し、フロー中立性（Flow Neutrality）という新しい性質を定義。タイムスライシング機構でBitcoin互換の枯渇耐性仮想チャネルを実現。GUC（Global Universal Composability）フレームワークで安全性を形式証明し、実装コストは~5%のオーバーヘッドに抑えた。
リサーチクエスチョン
RQ 1
仮想チャネルはどのようなDepletion攻撃に脆弱か？既存プロトコルで防げているか？
RQ 2
「フロー中立性（Flow Neutrality）」という性質でDepletion耐性を形式化できるか？
RQ 3
Bitcoin互換のままタイムスライシングでFlow Neutralityを達成できるか？
RQ 4
GUCフレームワークでの安全性証明は実用的なオーバーヘッドで成立するか？

仮想チャネルのDepletion問題

攻撃の仕組み

A—B—Cの仮想チャネルで、BがAに対して一方的に多数のHTLCを送り付け、A→C方向の残高を枯渇させる。AはBとの実チャネルでの支払い能力を失う。

なぜ難しいか

仮想チャネルの中継ノード（B）は中間でリバランスができない。実チャネルと仮想チャネルの残高が分離されているため、不均衡を直接補正する手段がない。

研究の手順
1
Depletion攻撃の形式化
仮想チャネルプロトコル（Perun・LN等）に対するDepletion攻撃を形式定義。攻撃者モデル（Byzantineノード）を設定し、どのような状態が「枯渇」であるかを数値的に定義する。
攻撃形式化
2
フロー中立性（Flow Neutrality）の定義
「中継ノードの実チャネル残高が仮想チャネルの利用によって一方的に消費されない」というフロー中立性を形式定義。これがDepletion耐性の十分条件であることを証明。
性質定義
3
タイムスライシング機構の設計
仮想チャネルの利用を時間スロットに分割し、各スロットで双方向フローが均衡するよう制約する。スロット終了時に残高精算を行いフロー中立性を保証。Bitcoin互換スクリプトで実現。
プロトコル設計
4
GUC安全性証明
Global Universal Composability (GUC)フレームワークで安全性を証明。Horcruxがフロー中立性・原子性・liveness を同時に満たすことを示す。HTLCと任意の上位プロトコルとの合成が安全であることを保証。
形式証明
5
シミュレーション評価（LNトポロジー）
LNトポロジーをシミュレートし、Horcruxのオーバーヘッド（on-chain TX数・通信ラウンド数）を計測。タイムスライシングのスロット長とオーバーヘッドのトレードオフを分析。
評価
主要結果
初
フロー中立性を
形式証明した仮想チャネル
~5%
タイムスライシングの
オーバーヘッド
GUC
安全性フレームワーク
（UCより強い合成保証）
Bitcoin
互換性
（スクリプト変更不要）
💡 Perun / LN との比較: 従来の仮想チャネル（Perun / LN virtual channels）はDepletion攻撃への形式的な耐性がなかった。Horcruxはこれを初めて解決し、仮想チャネルの実用化への重要な障壁を取り除いた。
課題と限界
⏰
タイムスライシングの同期コスト
スロット境界での精算には両者の協力が必要。一方がオフラインの場合、スロット境界を跨いだ処理が複雑になる。Sleepy CRAB（オフライン対応）のような追加機構が必要になる可能性。
📐
GUC証明の検証の複雑さ
GUC証明は技術的に高度で、独立した検証が困難。形式証明のコード（Coqなど）での機械検証は将来の課題として残されている。
🔒
全griefing攻撃を対象とするわけではない
フロー中立性はDepletion攻撃を防ぐが、他の形態のgriefing（HTLC hold等）は別問題。Channel Jammingと組み合わせた複合攻撃への対策は未検討。
📄 Paper 12 · Privacy / Differential Privacy

Twilight: A Differentially Private
Payment Channel Network

Maya Dotan, Saar Tochner, Aviv Zohar, Yossi Gilad — Hebrew University of Jerusalem
USENIX Security 2022
残高プロービング攻撃に対して（ε, δ）差分プライバシー（DP）の形式的保証を初めてLightningに適用。ノードがHTLC受諾を確率的に行う確率的受諾（Probabilistic Acceptance）を設計し、1000回のプローブで攻撃者が得られる精度をキャパシティの~2%に制限。Bitcoinスクリプト変更なしで展開可能であることを示した。
リサーチクエスチョン
RQ 1
差分プライバシー（DP）はLightningの残高プロービング防御に理論的保証を与えられるか？
RQ 2
HTLCの二値（成功/失敗）応答にDPを適用するにはどう設計すればよいか？
RQ 3
DP保護がネットワーク全体（マルチホップ）にcompositionされるとき保証はどう変化するか？
RQ 4
DP保護が正常な送金に与える成功率低下はどの程度か？実用範囲内か？

DP × Lightning の新しさ

従来防御の問題

レートリミット・エラー統一・Onionパディングはいずれもヒューリスティックで理論的保証なし。攻撃者がパラメータを調整すれば回避可能。

DPが与えるもの

ε-DPは「n回プローブしても攻撃者が得られる情報はε-bounded」という数学的証明付き保証。機械学習・統計の分野で広く確立されたフレームワーク。

研究の手順
1
プロービングをDPメカニズムとして定式化
残高プロービングを「残高Bへのクエリ」としてDP理論に落とし込む。攻撃者が得る「成功/失敗」応答を「残高に依存したランダム変数」として再定義。
理論的定式化
2
確率的受諾（Probabilistic Acceptance）の設計
ノードが要求額xに対して確率P[accept] = σ((B-x)/b)（sigmoidal関数）で受諾決定。残高B≫xなら確実に通し、B≪xなら確実に拒否、境界域はランダム。ラプラスノイズの離散版として機能。
プロトコル設計
3
（ε, δ）-DP保証の証明
確率的受諾が（ε, δ）-DPを満たすことを定理として証明。n回プローブ後の攻撃者の残高推定誤差がO(b√n)でboundされることを導出。
形式証明
4
ネットワークDPの合成分析
各ホップで独立にノイズ注入→DPの合成定理により全体の（ε, δ）を算出。攻撃者が複数ホップ情報を組み合わせた場合の保証を分析。εが加算される（composition）ことへの対応を設計。
合成分析
5
mainnetスケールでのシミュレーション評価
mainnetスナップショットを使い、各εパラメータで①攻撃者の残高推定誤差と②正常送金成功率を測定。ε=1〜3が実用的なスイートスポットであることを示す。
評価
主要結果
初
LNにDP理論を
系統的に適用した研究
~2%
1000 probes後の
推定誤差（ε=1）
-2〜5%
正常送金成功率の
低下（ε=1）
0
Bitcoin変更
（HTLC互換のまま）
εパラメータDP保護強度正常送金影響推奨用途
ε = 0.1非常に強い成功率 -10〜20%高セキュリティノード
ε = 1強い-2〜5%実用バランス
ε = 3中程度〜0%一般ルーティングノード
ε = 10+弱い影響なし実質DP無効
課題と限界
💊
単発クエリへの保護は弱い
DPは「繰り返しクエリの統計的保護」を対象とする。「このチャネルは今通るか？」という1回の試みには、DPは強い保証を与えない。Slow Jammingとの組み合わせが必要。
🤝
全ノードの協調展開が必要
DP防御は参加ノードが多いほど有効。「εの弱いノード」が経路上に存在すると、そこから残高情報が漏洩する。展開の段階的普及期間が脆弱になる。
⚙️
εの選択がノード個人の判断に委ねられる
各ノードが独立にεを設定できるため、ネットワーク全体の保証がバラバラになる。標準化なしでは「weak link」を探す攻撃者に悪用される可能性。
📄 Paper 13 · Security / DoS

Congestion Attacks in
Payment Channel Networks

Ayelet Mizrahi, Aviv Zohar — Hebrew University of Jerusalem
FC 2021 (Financial Cryptography)
Lightning Networkに対してわずか$30〜$1000の資本でネットワーク全体の送金成功率をほぼ0%に落とせることを初めて定量的に示した。HTLCのスロット制限（483/チャネル）と残高占有を悪用し、Scale-freeトポロジーの上位Hubを狙い撃ちにする最適戦略を提示。MPPや経路冗長化は解決策にならないことを示した。
リサーチクエスチョン
RQ 1
Lightning Network全体に対するDoS攻撃の現実的なコストはどの程度か？
RQ 2
Slot Exhaustion vs Value Exhaustion——どちらがより安価で効果的な攻撃か？
RQ 3
Scale-freeなLNトポロジーは攻撃を容易にするか？Hubを狙う最適戦略とは？
RQ 4
MPP・経路冗長化・Upfront feeなどの防御策は攻撃を無効化できるか？

2種類のJamming攻撃

Slot Exhaustion（スロット枯渇）

攻撃者が最小額HTLCを483個（上限）送り付けてスロットを全占有。自分宛てに送ってpreimageを出さずに保留。資本コストは微々たる額。

Value Exhaustion（残高枯渇）

大額HTLCでチャネルの流動性をまるごとlock。スロットが空でも残高がなければ送金不能。チャネル容量ぶんの資本が一時的に必要。

研究の手順
1
攻撃の形式化（最適化問題として定義）
予算制約下で「どのチャネルを狙えばネットワークへの影響が最大か」を最適化問題として定式化。目的関数 = 送金成功率の低下、制約 = 攻撃コスト≤予算B。
最適化定式化
2
LNトポロジー解析（Betweenness中心性）
2019年Lightningトポロジースナップショットを分析。Scale-free分布（少数Hubが多数の経路を中継）を確認。Betweenness中心性上位N個のHubが最小コスト最大破壊ターゲットであることを示す。
グラフ分析
3
シミュレーション（gossipスナップショット）
実LNデータ上でSlot/Value jamを上位N channelに仕掛けた場合の送金成功率・平均経路長・必要コストをシミュレート。攻撃前後の比較で破壊力を定量化。
シミュレーション
4
対策の評価（4カテゴリ）
①Upfront fees、②Reputation、③Stake-based、④Loop detection の各防御を評価。MPP・経路冗長化（5倍）も評価。いずれも上位Hub攻撃に対して効果が限定的であることを示す。
対策評価
主要結果
$30
上位50チャネルSlot jam
（成功率20%→0%）
$1,000
上位50チャネルValue jam
（同効果）
$5,000
ネットワーク完全停止
の推定コスト
×5冗長
経路冗長化も効果なし
（Hub集中型のため）
⚠️ SoK Jammingとの関係: 本論文（FC 2021）はJamming問題を「ネットワーク規模の現実的脅威」として確立した。後の [[SoK: Channel Jamming (Kotzer-Zohar 2024)]] はこの研究を起点に防御フレームワークを体系化した。同じHUJI Zoharグループによる研究継続の典型例。
課題と限界
🔬
シミュレーションベース（倫理的制約）
実際のmainnetへの攻撃は倫理的に実施不可。シミュレーションは実際のトラフィックパターン・ノード挙動・再試行ロジックを完全に再現できない。
📅
2019年データ（Anchor Outputs前）
Anchor Outputs（2020年以降）・MPP普及・Taproot Channelsなど大型変更後の現代LNでは攻撃コストや影響が変化している可能性がある。
👥
単一攻撃者モデル
複数攻撃者が協調または競合する場合の分析がない。攻撃者同士のゲーム理論的相互作用（攻撃資源の競合）は未考慮。
📄 Paper 14 · Game Theory / Miner Incentives

Suborn Channels:
Incentivizing Miners to Attack Lightning

Zeta Avarikioti, Orfeas Stefanos Thyfronitis Litos — IST Austria; TU Darmstadt
FC 2022 (Financial Cryptography)
Lightning/DMCのタイムロック機構が前提とする「rational minerは手数料の高い正直なTXを優先採掘する」という仮定を打破。タイムロック賄賂（Timelock Bribe）がNash均衡として成立する条件をゲーム理論で厳密に証明し、タイムロックの長さは万能薬でないことを示した。対策として担保自動報酬型Suborn Channelと動的手数料調整を提案。
リサーチクエスチョン
RQ 1
rational minerは賄賂でHTLCタイムロック攻撃に加担するか？Nash均衡として成立するか？
RQ 2
賄賂が「dominant strategy」になる最小賄賂額はどう計算できるか？タイムロック長に依存するか？
RQ 3
DMCとLNでそれぞれ攻撃が合理的になるチャネル残高差の条件は？
RQ 4
Suborn Channel設計と動的revocation fee調整で攻撃を経済的に無効化できるか？

なぜこれは見落とされていたか

従来の前提

LN仕様は「revocation TX はタイムロックなし → minerが即座に採掘する」と前提。この前提は「miner = 正直」または「手数料競争でrevocationが勝つ」を暗黙に仮定していた。

本論文の反論

攻撃者が「古いTXを採掘したら高額手数料を払う」と約束できる。これはフォーク不要・miner側リスクゼロの検閲攻撃。賄賂がrevocation fee × ~50倍を超えると Nash 均衡になる。

研究の手順
1
ゲーム理論モデルの構築（n rational miners）
n個のrational minerを仮定し、各minerのマイニングパワー比率λiを定常・公知として設定。各ラウンドでminerがTX採掘を選択するゲームをモデル化。
ゲームモデル
2
Nash均衡条件の導出（Theorem 1）
賄賂額f2がf2 > (f1 - mf) / λmin + mfを満たすとき、全minerにとって「正直なTXを無視し古いTXを採掘する」がstrict dominant strategyになることを証明。
均衡証明
3
DMC・LNへの適用（Theorem 2 / Theorem 5）
DMCとLNのそれぞれに対してbribe閾値条件を具体化。LNでは「古いstate残高 − 新state残高 > revocation fee × 50倍（λmin=0.02の場合）」が攻撃合理性の条件であることを示す。
プロトコル適用
4
対策の設計と有効性証明
①Suborn Channel（DMC向け）：攻撃時にAttackerのコインが自動的にMinerへの報酬になる設計。②動的revocation fee調整（LN向け）：被害者がrevocation TX手数料を動的に引き上げる。どちらも攻撃を経済的に無効化。
対策設計
5
手数料市場との関連分析
Bitcoin手数料水準が高い（ネットワーク混雑）ほど攻撃コストが増大することを閾値式から導出。逆説的に「高手数料環境はPCNの安全性を高める」という含意を分析。
経済分析
主要結果
×50
revocation fee比の
攻撃合理性閾値
独立
タイムロック長から
閾値が独立（驚きの結果）
0
攻撃失敗時の
Attackerのリスク
完全
動的fee調整で
攻撃を完全無効化
💡 最も驚くべき結果: 「タイムロックを長くすれば安全」という直感に反し、賄賂閾値はタイムロック長と完全に独立。十分な賄賂があればminerはいくらでも長く待ち続けるNash均衡が存在する。
比較項目Suborn (本論文)CRAB (Aumayr 2024)
攻撃者モデルRational partyByzantine party
対象プロトコルDMC + LNLN
防御機構Script変更 / 動的fee担保コイン（collateral）
オフライン対応考慮外Sleepy CRABで対応
課題と限界
⛏️
完全に rational minerの仮定
現実のマイニングプールは評判・法的リスク・コミュニティ圧力を考慮する。完全に経済合理性だけで動くrational minerは理想化された仮定。Pool operatorとpool minerの利害も分離している。
📊
λmin推定の不確かさ
最弱マイナーのパワーλminは動的に変化し、Botnetや秘密チャネルでの隠れたマイニングにより実際の値は不明。閾値計算の精度が限られる。
🔢
中程度の賄賂の未分析
f2*未満の中途半端な賄賂（一部minerが加担、一部が拒否）の均衡分析はfuture workとされた。現実の攻撃はこの「中程度」領域で起きる可能性がある。
📄 Paper 15 · Privacy / Empirical Analysis

An Empirical Analysis of Privacy in
the Lightning Network

George Kappos, Haaroon Yousaf, Ania M. Piotrowska, Sanket Kanjalkar, Sergi Delgado-Segura, Andrew Miller, Sarah Meiklejohn
FC 2021 (Financial Cryptography)
Lightningの「onion routing = privacy保護」という素朴な信仰をmainnet実データで完全に解体した初の大規模実証研究。4種類の攻撃（残高発見・送受信者推定・送金額推定・クロスレイヤー同一性紐付け）を組み合わせ、$1000〜2000の投資と自前ノード1台で大半の送金をdeanonymize可能であることを実証した。
リサーチクエスチョン
RQ 1
実際のmainnetで残高・送金額・送受信者は攻撃者に推定可能か？
RQ 2
オフチェーンの観察とオンチェーンのChain Analysisを組み合わせると何が分かるか？
RQ 3
攻撃に必要な資本・計算資源・時間はどの程度か？現実的な攻撃者範囲は？
RQ 4
Blinded Paths・BOLT 12・MPPは登場する前後でプライバシーはどう変化したか？

4つの攻撃の組み合わせ

攻撃手法成功率
残高発見二分探索プロービング100%（全テストチャネル）
送金額推定残高変動の時系列観察〜90%
送受信者リンク複数チャネルの同期残高変化〜50%
クロスレイヤー同一性funding TX のChain Analysis〜30%+
研究の手順
1
観測ノードの戦略的配備
自前でLightningノードを複数稼働し、高Betweenness Centralityの位置に配置。多数チャネルに接続して送金経路の大半が自ノードを通るように設定。$1000〜2000の投資。
観測インフラ
2
Gossipデータ収集・チャネルグラフ構築
BOLT 7 gossipプロトコル経由でネットワーク全体のチャネルグラフ（容量・fee・チャネルID）を収集。1ヶ月間の継続観測でグラフ変化を追跡。
データ収集
3
残高プロービング（大規模実施）
二分探索プロービングをmainnet全チャネルに対して実施（倫理的配慮のうえ）。チャネルの残高プロファイルを完全に作成。ground truth（自前チャネル）で精度を検証。
攻撃実施
4
送受信者推定（時間相関分析）
複数チャネルの残高を同時刻でスナップショット→差分を観察→同じ送金が通過した経路全体の「足跡」を時間相関でリンク。送信者・受信者ペアを〜50%の確率で特定。
プライバシー攻撃
5
クロスレイヤー分析（Chain Analysis）
チャネルのfunding TXをBitcoin Chain Analysisで解析（common-input heuristic・address reuse・取引所タギング）。ノード運用者のBitcoin identityを特定し、off-chain hopごとにidentityを貼り付け。
クロスレイヤー
主要結果
100%
残高発見成功率
（テスト全チャネル）
~90%
送金額推定
成功率
~50%
送受信者ペア
特定成功率
$1〜2K
攻撃に必要な
初期投資額
なぜこんなに脆弱だったか——5つの根本原因
📡
Gossipで公開情報が多すぎる
Capacity・fee・channel IDが全公開。攻撃者がグラフを完全に把握できる。
💰
プロービングがほぼ無料
失敗HTTPCには手数料ゼロ。繰り返し試行のコストが存在しない。
⏱️
残高変動が即時反映
送金成功後の残高変化が即座に観測可能。時間相関攻撃の土台。
課題と限界
📅
2019〜2020年データ（Blinded Paths以前）
BOLT 12のBlinded PathsやBOLT 4のRoute Blindingが普及した現代では攻撃③④の効果が低下。特に受信者identity紐付けは部分的に緩和されている。継続的な再評価が必要。
🎭
攻撃者は「active participant」が前提
高Betweennessポジションにノードを配置してチャネルを開設する必要がある。完全にpassiveな観察者（LNに参加しない）では攻撃①②③は成立しない。
📦
MPP普及後の精度低下
大口送金がMPPで多数の小口に分割される現代では、残高変動からの送金額・経路推定の精度が低下している。特に攻撃②③への影響が大きい。
💡 学術的意義: 本論文は「Lightningはプライバシー安全」というassertion based な信仰を実データで上書きした転換点。以降のプライバシー研究（Twilight/DP・BOLT 12・Blinded Paths）が全てデータベースでの議論になった。Tikhomirov・Kappos・Dotan の3論文がLN probing研究の三角形を形成している。