技術要約：FOベースKEMにおける検証可能な復号化テスト

問題提起

Fujisaki–Okamoto (FO) 変形に基づく耐量子計算機暗号（KEM）は、決定的な復号化チェックに依存している。すなわち、アルゴリズムは暗号文を復号し、暗号化の乱数を再導出し、暗号文を再計算し、共有秘密を導出する前に、受信した暗号文と比較しなければならない。このチェックはセキュリティ上極めて重要であるが、標準的なブラックボックス型の入出力テストでは、特定の実装上の欠陥を検出できない場合がある。実装が再暗号化計算の一部を省略したり、分岐選択ロジックを変更したりしても、正直な（honest）生成による暗号文に対しては期待される共有秘密を返し続けることがあり、その結果、標準的なテストハーネスにおいて失敗を発生させることなく、セキュリティチェックを実質的にバイパスしてしまう可能性がある。

本論文は、KEMに確認コード（confirmation codes）を付加した場合に、ブラックボックス・テストを用いてFOベースの復号化チェックの実行について、何が形式的に証明可能であるかという問いに取り組んでいる。

手法およびモデル

著者らは、**正直なリファレンス・ハーネス（honest-reference harness）**の下でテストされる、確認コード増強型FO復号化の形式理論を提案している。

増強された構成

このモデルは、最終的な鍵導出に隠された確認ウィットネス $W$ を導入することで、標準的なFOベースKEMを拡張したものである。

1. カプセル化（Encapsulation）: 暗号文と内部的な確認値 $W$ を生成する。最終的な鍵 $K$ は、$K = G_K(\langle \text{good}, B, W \rangle)$ として導出される。ここで $B$ は局所的なトランスクリプト接頭辞であり、$G_K$ はランダムオラクルである。
2. 復号化（Decapsulation）: 暗号文と確認ウィットネス $W'$ を再計算する。最終的な鍵は、$W' = W$ である場合にのみ導出される。
3. 正直なリファレンス・ハーネス: テストハーネスは復号化の入力（暗号文、鍵）を提供するが、隠されたウィットネス $W$ と最終的な鍵 $K$ は秘匿する。テスト対象システム（SUT）は、正しい鍵を生成するために、正しいタプル $\langle \text{good}, B, W \rangle$ を用いてランダムオラクル $G_K$ にクエリを発行しなければならない。

理論的枠組み

本論文は、SUTがランダムオラクルに対してクエリを行う候補となるウィットネスの集合を表す局所的な最終鍵クエリリスト $Q_G(B)$ を定義している。この手法の核心は、「リスト・ヒット（list-hit）」、すなわち隠されたウィットネス $W$ が $Q_G(B)$ に含まれるという事象の確率を分析することにより、欠陥のあるSUTがテストを通過してしまう（すなわち、正しい鍵を出力してしまう）確率を限定することにある。

分析では以下を区別している：

• 正直なリファレンス・テスト（Honest-Reference Testing）: SUTを、正当なリファレンスによって生成されたピアと比較する。
• 正直な自己テスト（Honest-Self Testing）: SUTをそれ自身（カプセル化と復号化の両方がSUTによるもの）と比較する。
• 依存性コーン（Dependency Cones）: 観測可能なターゲットベクトル（トランスクリプトと最終的な鍵）に実際に影響を与える操作の集合を特定する。

主な貢献

1. 厳密なリスト・ヒット検出定理

中心的な結果（定理5.1）は、任意の $q$-局所的なSUTについて、正直なリファレンス・ハーネスの下でのパス確率は以下によって抑えられることを確立している：
$$\text{Pass} \leq \delta_{\Pi_C} + \epsilon_{\text{alias}} + \epsilon_{\text{fresh}} + \Pr[W \in Q_G(B)] + 2^{-\kappa}$$
ここで：

• $\delta_{\Pi_C}$ は正直な正当性エラーである。
• $\epsilon_{\text{alias}}$ は敵対的なエイリアシング（最終鍵のエンコーディングにおける衝突）を考慮する。
• $\epsilon_{\text{fresh}}$ は最終鍵の鮮度欠陥（隠された点の漏洩）を考慮する。
• $\Pr[W \in Q_G(B)]$ はリスト・ヒット項であり、SUTが隠されたウィットネスを推測する確率を表す。
• $2^{-\kappa}$ はランダムオラクルの偶然の一致項である。

論文は、この境界がタイトであることを証明している（定理5.2）。すなわち、SUTのビューから $W$ を予測するいかなる予測器も、その成功率と一致するパス確率を持つ1クエリSUTを誘導する。したがって、リスト・ヒット項はハーネスによって測定される根本的な障害である。

2. リスト・ヒット項を限定する2つのルート

論文では、避けられないリスト-ヒット項を限定するための2つの異なる方法を提供している：

• ソース・セキュリティ・ルート（cUP-faithful）: ハーネスが「cUP-faithful（ソースの確認コード予測不可能性ゲームに対して忠実）」である場合、リスト・ヒット確率は $q \cdot \epsilon_{\text{cUP}}$ によって抑えられる。ここで $\epsilon_{\text{cUP}}$ はソースゲームにおける単一候補アドバンテージである。これにより、ソースのセキュリティ証明を、クエリ数の線形な損失を伴ってテストの文脈へと転送できる。
• エントロピー・ルート: ウィットネス $W$ がSUTのビューに対して平均条件付き最小エントロピー $\lambda$ を持つ場合、リスト・ヒット確率は $q \cdot 2^{-\lambda}$ によって抑えられる。このルートは、ソースのcUP境界が直接適用できない場合がある診断コード（例：切り詰められたハッシュ）にも対応している。

3. 依存性コーンの下界（負の結果）

本論文は、ブラックボックス認証の根本的な限界を証明している（定理5.37）。ある操作が**サポート活性依存性コーン（support-active dependency cone）**の外にある場合（すなわち、その操作を変更しても、正直なサポートにおける観測可能なトランスクリプトや最終的な鍵が変化しない場合）、その操作に対応する「消去（erasure）」（その操作をスキップするバージョンのコード）を含む実装クラスに対して、いかなるブラックボックス正直リファレンス・テストもその実行を証明することはできない。

• このような操作については、いかなるサーティファイア（certifier）の健全性（$\alpha$）と完全性（$\beta$）も $\alpha + \beta \geq 1$ を満たす。
• これは、追加のインストルメンテーション、不正な入力、またはより大きなターゲットセットがない限り、ブラックボックス・テストは、操作の実行と、その操作の消去を区別できないことを意味する。

4. 実装例とアーティファクト

理論は以下の2つのファミリーに実装されている：

• ML-KEM (FIPS 203): ソースの確認コード行（選択された非圧縮係数を使用）と、1バイトのハッシュコードを用いた診断アーティファクト・バリアント（ML-KEM-CD1）を分析する。
• HQC (2025年8月仕様): 確認コードが暗号文の末尾の切り詰め部分から派生する、ソルト付きFOバリアントを分析する。論文では、これらの末尾派生コードに対してリスト・ヒット項を限定するために必要な仮定である HQC-TailEnt を定義している。

著者らは、以下の内容を含む再現可能なアーティファクト FO-FaultBench を提供している：

• 固定されたベースライン（mlkem-native, HQC August 2025）。
• 変形バリアント（VSFO/CD1, CD*）。
• ミュータント・カタログ（結合故障、決定故障、対称故障）。
• 実験実行の凍結されたJSONLレコード。

実験結果

アーティファクトによるキャンペーンは、理論的主張を検証している：

• 結合故障（Binding Faults）: 確認コードを省略または上書きする故障は、正直なリファレンス・テストの下で検出される。これは、それらが最終的な鍵の入力を変化させるためである。
• 決定のみの故障（Decision-Only Faults）: 分岐選択のみに影響を与える故障（例：常に「good」な鍵を選択する）は、正直な暗号文の下では検出されないが、不正な入力や差分ハーネスの下では検出される。これは、サポート一致の制限を確認するものである。
• 対称故障（Symmetric Faults）: カプセル化と復号化の両方に適用される故障は、セルフテストは通過するが、正直なリファレンス・テストには失敗する。これは、ピア・モデルの必要性を実証している。
• 確率的推測: 確認コードを推測するミュータントは、保持されるコード長（$2^{-L}$）に応じてスケールする確率でパスする。これは、理論的なエントロピー境界と一致している。
• 範囲予算（Range Budgets）: HQCバリアント（CD1 vs. CD*）に関する実験は、保持される末尾ビット数を増やす（5ビットから37ビットへ）ことで、推測ミュータントのパス確率が大幅に減少することを示しており、エントロピー・ルートを検証している。

意義および主張

本論文は、FOベースのKEMに対して、ブラックボックス・テストが何を証明でき、何を証明できないかを正確に記述する確認コード・テストの形式理論を提供することを主張している。

• 肯定的な主張: 本論文は、確認コードの結合が、再暗号化の故障に対して検出可能な信号を作成することを確立している。ただし、それはリスト・ヒット項がソースのcUPまたは条件付きエントロピーによって限定される場合に限られる。また、実験結果を解釈するための厳密なフレームワークを提供する。
• 否定的な主張: 著者らは、ブラックボックスの正直なリファレンス・テストには固有の限界があることを明示している。それは、依存性コーンの外にある操作（例：一部の係数のみが結合されている場合の完全な再暗号化の実行）を、ハーネスのターゲットを変更するかインストルメンテーションを追加することなしに証明することはできない。
• 謙虚な姿勢: 著者らは、これらの定理が古典的なランダムオラクルモデル（ROM）の記述であることを強調している。彼らは基礎となるKEMのIND-CCAセキュリティを再証明するのではなく、構成レベルのセキュリティについては引用されたソース分析に依拠している。「セキュリティ」の性質は、構成のソースから継承されるものであり、本論文の貢献は、テスト信号および特定のハーネス構成下でのパス確率の解釈である。

本研究は、理論的なセキュリティゲーム（cUP, fCOR）と実用的な実装テストとの間の架け橋として機能し、ポスト量子KEMの実装に関する実験結果を解釈するための「主張の文法（claim grammar）」を提供するものである。