Signal Protocol and Post-Quantum Ratchets

📄 Summarized by Claude Sonnet 4.5

02 Oct 2025

どんなもの？

ユーザー体験を変えることなく、将来の量子コンピュータの脅威から通信を保護

既存のセキュリティ保証を維持しながら、段階的にロールアウト可能な設計

先行研究と比べてどこがすごい？

以前発表したPQXDHは初期セッション確立時のみ量子耐性を提供したが、SPQRは通信セッション全体を通じて継続的な量子耐性を実現

ML-KEM 768の内部構造を分析し、Encapsulation KeyとCiphertextの送信を部分的に並列化するML-KEM Braidプロトコルを開発

消去符号（erasure codes）を活用してデータをチャンク化し、メッセージ損失や攻撃者による妨害に対して堅牢性を確保

複数のエポックの秘密鍵を同時に保持することによるセキュリティリスクを避けるため、シミュレーションを通じて最適なステートマシン設計を選択

技術や手法のキモはどこ？

ML-KEM（Key-Encapsulation Mechanism）を用いた非対称的な鍵共有メカニズムの実装

EK（1184バイト）の32バイトのSeedとハッシュ（合計64バイト）を先行送信し、残りのEK（EK2）とCTの大部分（CT1）を並列送信することで効率化

消去符号により大きなデータを小さなチャンクに分割

任意のN個のチャンクで元のメッセージを復元可能にすることで、パケット損失や悪意ある中間者攻撃に対抗

両方のプロトコルを破らない限り、混合鍵を乱数と区別できないハイブリッドセキュリティを実現

後方互換性のあるダウングレードメカニズム

セッション確立の最初のメッセージ交換時のみダウングレードを許可し、その後はSPQRの使用を固定

どうやって有効だと検証した？

Eurocrypt 2025で消去符号ベースのチャンク化とTriple Ratchetプロトコルの理論的安全性を証明

USENIX Security 2025で6つの異なるポスト量子ラチェットプロトコルを分析・比較し、SPQRが最適であることを実証

ProVerifを用いた形式検証をプロトコル設計プロセスの中核に組み込み

約12種類のプロトコル候補をモデル化し、必要なセキュリティ特性を機械検証

haxを使用してRust実装をF*に変換し、CIパイプラインで継続的に形式検証を実行

実装の正確性、事前条件・事後条件の保証、パニックフリーであることを証明

様々なメッセージ送信比率、パケット損失、順序変更などの条件下でステートマシンのシミュレーションを実施

侵害時点で露出するエポックの秘密鍵数を追跡し、最もセキュアな設計を選定

議論はある？

セッションは潜在的に数年間続く可能性があるため、全てのセッションがSPQR保護されるには時間がかかる

将来的に全クライアントがサポートした後、SPQRを持たないセッションをアーカイブする更新を展開予定

ML-KEMのEKとCTのサイズ（それぞれ1184バイトと1088バイト）はECDHの32バイトと比較して大きく、帯域幅の制約がある環境では課題

ML-KEM Braidと消去符号により、メッセージあたりの追加オーバーヘッドを最小化

形式検証は開発プロセスの一部として継続的に実施されるため、コードベースが凍結されることはなく、将来の更新も検証可能

同じダウングレードメカニズムにより、将来的にSPQRv2などへのアップグレードも可能な設計