Beyond the Finite Variant Property: Extending Symbolic Diffie-Hellman Group Models (Extended Version)

技術要約：有限バリアント特性を超えて：記号的ディフィー・ヘルマン群モデルの拡張

問題提起
ディフィー・ヘルマン（DH）群は現代の暗号プロトコルの基礎であるが、最先端の記号的プロトコル検証器（Tamarin、Proverif、Maude-NPAなど）は、その代数的な性質を完全にはサポートしていない。これらのツールは指数演算や指数の乗算をモデル化することはできるが、指数の加算に対応する「群要素の乗算」をモデル化することは一般にできない。この制限は、完全なDH群を記述する等式理論（分配法則、結合法則、および交換法則を含む）が、単一化問題（unification problem）を決定不能かつ無限的なものにするという事実に起因している。その結果、既存のツールは、アドバーサリ（攻撃者）や正当な当事者が指数の完全な体構造を利用するプロトコル（例：ElGamal暗号やMQV鍵共有）について推論することができない。

手法
著者らは、完全なDH群構造を利用するプロトコルのセキュリティ特性を検証するための半決定手続きを提案している。このアプローチは、記号的な推論と代数的な手法を統合したものであり、Tamarinプルーバーへの拡張として実装されている。

1. 理論的基礎： 本研究は、DoughertyとGuttmanによって提案された書き換えシステムに基づいており、これは結合法則および交換法則（AC）を考慮した収束的な書き換えシステム（$\to_{DH}$）を用いて体を近似するものである。このシステムにより、項の正規形を定義することが可能となる。
2. 非キャンセル仮定： このアプローチは、主に2つの条件に基づいている。
   • C1： すべての群要素は、共通の生成子を持つ単一の固定された群に属すること。
   • C2（非キャンセル）： セキュリティ特性は、部分項が互いに打ち消し合わない（すなわち、単位元1または0に簡約されない）項を含むものであること。この条件が満たされない場合、ツールは有効な攻撃を見つけることはできるが、セキュリティの証明には、特定の項がキャンセルされないことを手動で検証する必要がある。
3. ハイブリッド制約解決： コアとなる革新は、DH項に対する直接的な単一化を回避する修正制約解決アルゴリズムである。代わりに、以下の2段階のプロセスを採用している。
   • 記号的単一化（簡略化された理論）： アルゴリズムは、まず群乗算演算子を除外した簡略化された等式理論（$\varepsilon_{simp}$）内で項を単一化する。これにより、既存のTamarinの単一化アルゴリズムを使用してルート項をマッチさせることが可能になる。
   • 代数的再構成： ルート項がマッチした後、アルゴリズムは記号的な項を代数的なオブジェクト（体上の多項式）として解釈する。指数を「漏洩した（アドバーサリが既知の）」ものと「秘密の」ものに分類する。ガウス消去法（または非線形ケースの場合はBuchbergerのアルゴリズム）を用いて、秘密の指数がターゲットとなる項を再構成するために、漏洩した指数とどのように組み合わせられるかを解く。
4. インジケーター関数： 項が導出可能であるかを判断するために、著者らは「インジケーター」関数を定義している。これは、項を構築するために必要な最小限の秘密成分を特定する。もし、いずれかのインジケーターがアドバーサリの知識から再構成できない場合、その項は導出不能であるとみなされる。
5. アドバーサリ・モデリング： この拡張は、すべてのDH演算を適用できる能動的なDolev-Yaoアドバーサリをサポートしている。制約解決器は、項の多項式解釈から導出された線形方程式を、アドバーサリが満たすことができるかどうかをチェックすることで、アドバーサリによる推論を処理する。

主な貢献

• 完全なDH理論のための初の自動化ツール： 本研究は、群要素の乗算を含む、完全なディフィー・ヘルマン群構造を利用するプロトコルをモデル化し、推論することができる自動検証ツールを実現した最初の実装である。
• 健全性と完全性： 著者らは、拡張された制約解決関係が（非キャンセル仮定の下で）健全かつ完全であることを証明している。Tamarinが攻撃を見つけた場合、それは有効な実行であり、セキュリティを証明した場合、記号モデル内において違反する実行は存在しない。
• Tamarinへの統合： このアプローチは、Tamarinの制約解決アルゴリズムを修正し、DHソートされた項に対する標準的な単一化ルールを代数的な解決ステップに置き換える新しいルール（$C@, C_{Prem}, C=, C_{var}$）を追加することで実装されている。
• 混合理論の処理： この手法は、他のユーザー定義の等式理論（例：対称暗号、ペア）と完全なDH理論を組み合わせることをサポートしており、これは結合された項を「クリーニング」すること（単一化のためにDH部分項を新鮮な変数に置き換え、その後、代数的解決のためにDH制約を再導入すること）によって実現される。

結果とケーススタディ
著者らは、いくつかのプロトコルを用いてこの実装を評価した。

• ElGamal暗号： 本ツールは、ElGamal暗号スキームの実行可能性と秘匿性を正常に証明した。特筆すべきは、完全なDHサポートを伴う記号モデルにおいて、ElGamalが自動的に検証されたのはこれが初めてである点である。また、イニシエータが認証されていない場合に、秘匿性が欠如していることも正しく特定した。
• MQV鍵共有： 本ツールは、MQVプロトコルの分析に使用された。ツールは、Kaliskiによる既知の「未知鍵共有（unknown key-share）」攻撃を再発見することに成功し、複合的な群要素を含む複雑な攻撃を見つける能力を実証した。
• ベンチマーク評価： この拡張は、20の既存のTamarinモデル（WireGuardや様々な鍵共有プロトコルを含む、制限されたDH理論を使用していたもの）に対してテストされた。結果として、この拡張はこれらのプロトコルに対して制限された理論と同じセキュリティ判定を生成することを示したが、拡張された探索空間の複雑さにより、実行時間は増加した。

意義
本論文は、本研究が記号的プロトコル検証における重要な進歩であることを主張している。完全なDH理論における単一化の決定不能性を克服することで、著者らは、ディフィー・ヘルマン群の完全な代数構造に依存する、より広範なクラスの暗号プロトコルの自動検証を可能にした。ElGamalを自動検証し、MQV攻撃を数分以内に再発見できる能力は、このアプローチの実現可能性、スケーラビリティ、および効率性を示しており、理論的な代数的性質と実用的な自動セキュリティ分析の間の溝を埋めるものである。