HKHiago Kin Levi

Research / Paper Files

Paper Files

Paper Files は、学習ツールとして scientific method を適用する、cybersecurity における継続学習の個人的実践です。各記事は学術出版のためではなく、斧を研ぐための意図的な訓練として書かれています。特定トピックへの知識を深め、考えを厳密に整理し、特定の विषयへの理解が時間とともにどう発展するかを観察するためです。これは訓練日誌に相当する知的活動であり、各エントリには何を学び、どのように分析し、どのような結論に至ったかが記録されます。

私は、セキュリティ専門家がこの方法を採用することを強く推奨します。習得したいトピックを一つ選び、一次資料 (RFCs、papers、公式ドキュメント) を調査し、文章を序論、方法論、分析、結論で構成し、同僚に説明するつもりで書いてください。書くという行為は思考の明確さを強制し、受動的な読書では見えない理解の穴をあぶり出します。このサイトの記事を形式と深さの例として活用し、自分自身のコレクションを構築してください。時間が経てば、どのコースや certification でも置き換えられない、洗練された知識の個人リポジトリが手に入ります。

DAI & ADAI · 2026

DAI · EN

DAI: A Domain-Specific LLM with Model-Excluded Authority, Capability-Disjoint Verification, and Recomputable Receipts

DAI (Decripte Artificial Intelligence) is a proprietary domain-specific LLM within a governed autonomous defensive architecture. It is an instance of the proposed ADAI category defined in the companion framework paper. T…

Read paper →ADAI · EN

Autonomous Defensive AI: An Envelope-and-Evidence Framework for Governed LLMs Acting on Production Infrastructure

ADAI (Autonomous Defensive Artificial Intelligence) is a proposed category of governed autonomous cyber defense. The framework specifies defended perimeters, bounded effects, declared rollback and capability-disjoint ver…

Read paper →
すべてDetectionDFIRAppSecDevSecOpsAI SecurityIAMCloudContainersIRCryptoResearchPhishingSecrets

11 papers

Crypto

タイトル: 高度な脅威に対するレジリエントな暗号アーキテクチャ: 企業インフラにおけるCrypto-Agile制御の形式化、実装、および運用評価

タイトル: 高度な脅威に対するレジリエントな暗号アーキテクチャ: 企業インフラにおけるCrypto-Agile制御の形式化、実装、および運用評価 要旨: 現代の企業インフラにおいて暗号メカニズムへの依存が増大したことで、暗号技術はデジタル・トラストの主要な基盤となった。しかし、暗号ライブラリの悪用を伴う近時のインシデント（例: OpenSSL における CVE-2022-0778）、プロトコルに対する攻撃（例: TLS に対する downgrade attacks）、および ransomware による暗号の運用上の悪用（MITRE ATT&CK T1486）は、暗号理論と実装実務の間に存在するギャップを明らかにしている。本研究は、能動的脅威下にある企業環境における暗号資産のガバナンス、検知、およびレジリエンスの問題を体系的に検討する。私たちは、深層防御を志向した crypto-agile アーキテクチャを提案し、暗号資産の自動発見、パラメータの形式的検証、ネットワーク上の暗号異常検知、およびインシデントへの自動対応を統合する。 本手法は、セキュリティ特性（機密性、完全性、forward secrecy）の形式解析、Suricata および Zeek によるトラフィック計測、OpenSSL および CFSSL による証明書検証、Volatility によるメモリ解析、そして Sigma と Elastic Stack によるイベント相関を組み合わせる。私たちは二つの主要アルゴリズムを開発した。(i) Crypto Asset Discovery and Risk Scoring (CADRS) は、インベントリ作成とリスク優先順位付けのためのものであり、(ii) Crypto Misuse Anomaly Detection (CMAD) は、TLS セッションにおける異常パターンおよび暗号プリミティブの不正利用を識別するためのものである。 1,200 の資産と 18 TB の TLS トラフィックを有する環境で実施した実験評価により、不安全な設定の特定に要する平均時間が 63% 短縮され、ダウングレードに脆弱な TLS セッションの 94.7% を 3.1% の偽陽性率で検知できることが示された。提案アーキテクチャのネットワークスループットに対する平均オーバーヘッドは 4.8% 未満であった。実際の ransomware シナリオに基づくケーススタディでは、データの完全な exfiltration の前に、悪意ある暗号利用パターンを識別できることが実証された。 我々は、暗号の形式化、運用テレメトリ、および応答自動化の統合が、暗号攻撃面を縮小するうえで不可欠であると結論づける。本研究は、企業における暗号レジリエンスに対して実践的かつ測定可能なアプローチを提供し、セキュリティチーム、SOC、ならびにインフラ・アーキテクト向けの運用指針を提示する。

Read paper →Crypto

タイトル: 重要インフラ向けのレジリエントな暗号アーキテクチャ：形式モデリング、アクティブディフェンス、および高度な脅威に対する実証的評価

タイトル: 重要インフラ向けのレジリエントな暗号アーキテクチャ：形式モデリング、アクティブディフェンス、および高度な脅威に対する実証的評価 要旨: サイバー諜報キャンペーン、ランサムウェア、およびハイブリッド作戦の高度化は、企業システムおよび重要インフラにおける暗号実装の構造的脆弱性を露呈させてきた。TLS の誤設定、秘密鍵の侵害、脆弱な楕円曲線の不適切な使用、ならびに OpenSSL などのライブラリに対する攻撃（例: CVE-2014-0160 – Heartbleed）を含む事案は、暗号セキュリティがアルゴリズムの数学的堅牢性だけでなく、その実装、鍵管理、および運用統合に依存することを示している。本研究では、次の三つの柱に基づくレジリエントな暗号アーキテクチャを提案する。(i) MITRE ATT&CK に基づく現実的な能力を備えた敵対者の形式モデル化、(ii) 継続的な暗号学的検証を伴う鍵ローテーションと検証の自動オーケストレーション、(iii) ネットワーク・テレメトリおよび行動分析による暗号劣化のアクティブ監視である。我々は、HSM、カスタム provider を備えた OpenSSL 3.x、Suricata、Zeek、ならびに YARA と Sigma に基づく検知モジュールを統合した実験フレームワークを開発した。 本ソリューションを、分散された 120 ノードを備える制御環境で評価し、プロトコルのダウングレード（T1190）、暗号化チャネルを介したエクスフィルトレーション（T1041）、および暗号資材の侵害（T1552）といった攻撃をシミュレートした。その結果、暗号異常の平均検知時間（MTTD）が 73% 短縮され、無効または期限切れの証明書の使用試行の 92% が自動的に緩和された。ECDHE-RSA-AES256-GCM-SHA384 を用いた TLS ワークロードにおける平均性能オーバーヘッドは 4.8% 未満にとどまった。我々の貢献は以下のとおりである。(C1) 運用上の暗号劣化問題に関する数学的定式化、(C2) セキュリティ特性の継続的検証アルゴリズム、(C3) アーキテクチャの有効性に関する定量的な実証的証拠である。これらの結果は、運用上の暗号セキュリティには、形式理論、安全なエンジニアリング、ならびにテレメトリに基づくアクティブディフェンスの統合が必要であることを示している。

Read paper →Crypto

分散インフラストラクチャのための適応的かつ検証可能な暗号アーキテクチャ：形式化、実装、および高度な脅威モデル下での実証的評価

TITLE: 分散インフラストラクチャのための適応的かつ検証可能な暗号アーキテクチャ：形式化、実装、および高度な脅威モデル下での実証的評価 ABSTRACT: クラウドサービス、ブロックチェーンネットワーク、サイバーフィジカルシステムを含む分散インフラストラクチャにおける暗号技術の大規模な導入は、実装、設定、および暗号構成の不備の悪用が比例して増大することを伴ってきた。証明書の不適切な検証、AEADプロトコルにおけるnonceの再利用、ならびに CVE-2022-0778（OpenSSL）のような脆弱性に関連する最近の事例は、形式的安全性と運用上の安全性との間のギャップを示している。本研究では、大規模な分散環境における体系的な障害を緩和することを目的とした、適応的かつ検証可能な暗号アーキテクチャ（ACAV）を提案する。我々のアプローチは、(i) 時相論理に基づく暗号特性の形式的検証、(ii) リスク指向の適応的鍵ローテーション、(iii) 異常検知を伴う暗号利用の継続的監視、を統合する。問題を、遅延およびスループットの制約の下で残留リスク R(t) を最小化する多目的最適化として定式化する。我々は、Kubernetes、OpenSSL 3.0、および FIPS 140-3 準拠の HSM モジュール上にプロトタイプを実装し、64ノードのクラスタで評価した。実験結果は、拡張 Dolev-Yao モデル下における鍵漏えいリスクの推定値が47.3%低減し、平均遅延オーバーヘッドは3.8%（±0.6%）、10,000同時接続を伴う TLS 1.3 ワークロードに対するスループットへの影響は2.1%未満であることを示した。静的な定期ローテーションポリシーと比較して、ACAV は暗号資材の不正再利用イベントを92%削減した。以上より、形式的検証、暗号テレメトリ、動的適応の体系的統合は、現代のインフラストラクチャにおける暗号耐性を強化するための実行可能かつスケーラブルな戦略であると結論づける。

Read paper →Crypto

CryptoResilient：分散インフラストラクチャにおける高度攻撃緩和のための適応的かつ形式的検証可能な暗号アーキテクチャ

本研究は、分散インフラストラクチャにおいて暗号技術を単なる保護手段としてではなく、脅威状況に応じて再構成可能な制御対象として扱う適応的な暗号アーキテクチャを提案する。従来、機密性や完全性を担保する暗号プリミティブは、理論上の安全性に基づいて評価されてきたが、実運用環境では、鍵管理、実装欠陥、認証情報漏えい、再送制御の不備、ならびに運用ポリシーの硬直性が複合的に作用し、システム全体の安全性を損なうことがある。本稿では、観測可能なリスク指標に基づいて鍵更新や暗号パラメータの再設定を行う CryptoResilient を提案し、さらに、継続的な形式検証を運用サイクルに組み込む枠組みを与える。提案手法は、リスク監視、ポリシー判定、暗号オーケストレーション、および SMT ベースの不変条件検証を結合し、鍵の時間的露出を抑制しつつ、攻撃者によるセッション再利用や秘密情報の長期滞留を抑えることを目的とする。加えて、Dolev–Yao 型の対向者モデルを拡張し、部分的侵害と時間的観測を許容する確率的脅威モデルの下で、適応的ローテーションの有効性を形式化する。試作実装と評価では、固定周期方式と比較して平均露出時間が短縮され、リプレイ攻撃に対する耐性が改善されることを示した。本研究は、暗号アルゴリズムの強度のみでは十分ではないという認識に基づき、運用時における暗号の適応性と検証可能性を両立させる設計原則を提示するものである。

Read paper →Crypto

ハイブリッド・インフラにおける行動暗号解析と適応的鍵監視：高度持続的脅威に耐性を持つ暗号アーキテクチャ

TITLE: ハイブリッド・インフラにおける行動暗号解析と適応的鍵監視：高度持続的脅威に耐性を持つ暗号アーキテクチャ ABSTRACT: オンプレミス環境、パブリッククラウドおよびプライベートクラウド、エッジコンピューティング、ならびに人工知能ベースのワークロードを組み合わせたハイブリッド・インフラの複雑性の高まりは、2025年における暗号セキュリティに新たな課題を課している。Zero Trust アーキテクチャの拡大、耐量子暗号の採用、および大規模言語モデル（LLMs）の大量利用は、攻撃対象領域を拡大させ、とりわけ暗号鍵の管理とライフサイクルに関してその影響が顕著である。本研究では、ハイブリッド・インフラにおける高度持続的脅威（APTs）を検知・緩和することを目的として設計された、行動暗号解析の形式的アーキテクチャと適応的鍵監視を組み合わせた提案を示す。我々は、ゲームベースの形式的セキュリティモデル、行動逸脱の確率解析、および暗号不変条件によるセキュリティ特性の検証に基づいて本提案を定式化する。さらに、統計的ダイバージェンスと、データ汚染に対して堅牢な機械学習に基づく検知モデルを導入し、eBPF、CNAPPs（Cloud-Native Application Protection Platforms）、および FIPS 140-3 に準拠した鍵管理システムから得られるテレメトリを統合する。我々は、鍵の外部流出、Kubernetes クラスタにおけるラテラルムーブメント攻撃、MLOps パイプラインの悪用を含む現実的なシナリオ下で本アーキテクチャを評価した。その結果、平均検知時間（MTTD）の有意な短縮と、適応的な攻撃者モデルの下での機密性および完全性の保証強化が示された。さらに、本提案が CRYSTALS-Kyber および CRYSTALS-Dilithium のような NIST 標準化の耐量子アルゴリズムと互換であり、形式的なセキュリティ特性を保持することも示した。以上より、行動暗号解析と適応的監視の統合は、現代のデジタル生態系における耐障害性の高い暗号防御の有望なパラダイムであると結論づける。

Read paper →Crypto

タイトル: ハイブリッド・インフラストラクチャにおける行動暗号解析と適応的鍵監視：高度持続的脅威に耐性を持つ暗号アーキテクチャ

タイトル: ハイブリッド・インフラストラクチャにおける行動暗号解析と適応的鍵監視：高度持続的脅威に耐性を持つ暗号アーキテクチャ 要旨: オンプレミス環境、パブリックおよびプライベートクラウド、エッジコンピューティング、ならびに人工知能ベースのワークロードを組み合わせるハイブリッド・インフラストラクチャの複雑性の高まりは、2025年における暗号セキュリティに新たな課題を突きつけている。Zero Trustアーキテクチャの拡大、耐量子暗号の採用、そして大規模言語モデル（LLMs）の大規模利用により、攻撃対象領域は拡大しており、とりわけ暗号鍵の管理およびライフサイクルに関して顕著である。本研究では、ハイブリッド・インフラストラクチャにおける高度持続的脅威（APTs）を検出・緩和するために設計された、行動暗号解析と適応的鍵監視を組み合わせた形式的アーキテクチャを提案する。我々は、ゲーム理論に基づく形式的セキュリティモデル、行動的逸脱の確率解析、ならびに暗号不変量を通じたセキュリティ特性の検証に基づいて本提案を位置づける。さらに、統計的ダイバージェンスとデータ汚染に対して頑健な機械学習に基づく検出数学モデルを導入し、eBPF、CNAPPs（Cloud-Native Application Protection Platforms）、およびFIPS 140-3に準拠した鍵管理システムから得られるテレメトリを統合する。私たちは、鍵の流出、Kubernetesクラスタにおける横展開攻撃、ならびにMLOpsパイプラインの悪用を含む現実的なシナリオの下で本アーキテクチャを評価した。その結果、平均検出時間（MTTD）の有意な短縮と、適応的敵対者モデルの下での機密性および完全性保証の強化が示された。さらに、CRYSTALS-KyberおよびCRYSTALS-DilithiumのようなNIST標準化済みの耐量子アルゴリズムとの互換性を実証し、形式的なセキュリティ特性が保持されることを示した。以上より、行動暗号解析と適応的監視の統合は、現代のデジタル・エコシステムにおける耐性のある暗号防御の有望なパラダイムであると結論づける。

Read paper →Crypto

CriptoResiliente: 大規模分散環境における暗号的障害緩和のための適応型かつ形式検証されたアーキテクチャ

TITLE: CriptoResiliente: 大規模分散環境における暗号的障害緩和のための適応型かつ形式検証されたアーキテクチャ ABSTRACT: 現代の暗号技術は分散システムのセキュリティの基盤を構成し、機密性、完全性、真正性、および否認防止を保証する。AES、RSA、ECDSA、および TLS 1.3 プロトコルのようなプリミティブは古典的計算仮定の下では依然として形式的に安全であるが、経験的には大多数のインシデントが実装、設定、鍵管理、およびシステム統合の不備に起因することが示されている。2025年には、NIST のポスト量子標準への移行、クラウドネイティブアーキテクチャの大規模採用、CNAPP（Cloud-Native Application Protection Platforms）、eBPF によるインストルメンテーション、さらに IA/LLMs ベースのコンポーネントの組み込みにより、攻撃対象領域と運用上の複雑性が大幅に拡大している。本研究では、CriptoResiliente を提案する。これは、大規模分散環境における暗号的障害を緩和するために設計された、インクリメンタルな形式検証を備えた適応型暗号アーキテクチャである。我々は、暗号鍵に対する数学的リスクモデル $R(k,t)$ を導入し、曝露時間、関連する脆弱性、および観測された攻撃強度を組み込むとともに、計算コスト制約下での最適化問題として定式化する。ネットワーク制御およびノードの部分的侵害を伴う敵対者モデルの下で、リスク指向の鍵ローテーションポリシーが平均曝露時間を大幅に削減することを示す。Kubernetes 1.29 上において、ハイブリッド TLS 1.3（X25519 + ML-KEM）、FIPS 140-3 互換 HSM との統合、eBPF および Prometheus によるテレメトリ、ならびに ProVerif による形式検証を備えたプロトタイプを実装した。最大 $10^7$ TLS セッション/日までの実験評価において、平均曝露時間が 73,4% 削減され、オーバーヘッドは 10% 未満であり、統計的有意性（$p < 0{,}01$）が確認された。結論として、暗号アジリティ、リスク指向モニタリング、およびインクリメンタルな形式検証の組み合わせは、2025年におけるレジリエントな暗号セキュリティのための実用的かつスケーラブルなアプローチであり、ポスト量子移行および AI ガバナンスの要件下においても有効である。

Read paper →Crypto

タイトル: CriptoResiliente: 高規模分散環境における暗号失敗の緩和のための適応型かつ形式的に検証されたアーキテクチャ

タイトル: CriptoResiliente: 高規模分散環境における暗号失敗の緩和のための適応型かつ形式的に検証されたアーキテクチャ 要旨: 現代暗号は分散システムのセキュリティの礎であり、機密性、完全性、真正性、否認防止を保証する。AES、RSA、ECDSA、TLS 1.3 プロトコルのような原始技術は、古典的な計算仮定の下では依然として形式的に安全であるものの、実証的経験は、インシデントの大半が実装、設定、鍵管理、システム統合の失敗に起因することを示している。2025年において、NIST のポスト量子標準への移行、クラウドネイティブ・アーキテクチャの大規模な採用、CNAPP（Cloud-Native Application Protection Platforms）、eBPF による計測、ならびに AI/LLM ベースのコンポーネントの組み込みは、攻撃対象領域と運用上の複雑性を大幅に拡大する。本研究では、高規模分散環境における暗号失敗を緩和するよう設計された、増分的な形式検証を備える適応型暗号アーキテクチャ CriptoResiliente を提案する。われわれは、露出時間、関連脆弱性、観測された攻撃強度を組み込んだ暗号鍵のためのリスク数学モデル R(k,t) を導入し、計算コスト制約付きの最適化問題を定式化する。ネットワーク制御およびノードの部分的侵害を伴う敵対者モデルの下で、リスク指向のローテーションポリシーが平均露出時間を大幅に削減することを示す。Kubernetes 1.29 上において、TLS 1.3 ハイブリッド（X25519 + ML-KEM）、FIPS 140-3 互換 HSM との統合、eBPF および Prometheus によるテレメトリ、さらに ProVerif による形式検証を備えたプロトタイプを実装した。1日あたり最大 10^7 の TLS セッションを用いた実験評価では、平均露出時間が 73.4% 減少し、オーバーヘッドは 10% 未満であり、統計的有意性（p < 0.01）を確認した。以上より、暗号アジリティ、リスク指向モニタリング、増分的形式検証の組合せは、2025年におけるレジリエントな暗号セキュリティ、ならびにポスト量子移行要件および AI ガバナンス下でも、有効で拡張可能なアプローチであると結論づける。

Read paper →Crypto

分散型重要インフラストラクチャのためのポスト量子完全性証明を備えた適応型暗号アーキテクチャ

TITLE: 分散型重要インフラストラクチャのためのポスト量子完全性証明を備えた適応型暗号アーキテクチャ ABSTRACT: ポスト量子暗号への移行は、特に移行期間中に相互運用性、性能、および形式的なセキュリティ保証を維持する必要性を考慮すると、分散型重要インフラストラクチャのセキュリティに重大な課題をもたらす。本研究では、適応型暗号アーキテクチャとポスト量子完全性証明（ACAPQ）を提案する。これは、古典的プリミティブとポスト量子プリミティブを、継続的な完全性の形式的アテステーション機構と組み合わせたハイブリッドモデルである。機密性は、ECDHE と CRYSTALS-Kyber の堅牢な合成に基づき、ハンドシェイクの完全なトランスクリプトによって認証された HKDF を用いた鍵導出により実現し、ダウングレード攻撃を緩和する。状態の完全性および真正性のために、Merkle 木と CRYSTALS-Dilithium 署名に基づくアテステーションプロトコルを導入し、第二原像耐性および EUF-CMA の下で定量化可能な確率的保証を提供する。脅威モデルは計算パラダイムにおいて定式化され、能動的傍受能力、適応的部分侵害、および BQP クラスによってモデル化される量子計算能力を有する確率的多項式時間 adversary を仮定する。ハイブリッド秘密の統計的独立性の仮定の下で、古典的プリミティブが将来的に破られた場合でも、導出鍵が識別不能性を維持することを示す。Go 1.22 と liboqs を用いてプロトタイプを実装し、Kubernetes 1.29 環境において毎秒 50,000 リクエストの負荷下で性能評価を行った。結果は、従来の TLS 1.3 と比較してレイテンシおよびスループットのオーバーヘッドが 12% 未満でありながら、改ざん検出率が 99% 以上を維持することを示した。さらに、CNAPP、クラウドネイティブ環境、セキュアな可観測性のための eBPF の利用、および 2025 年までの NIST と ENISA の指針に整合した暗号ガバナンスへの含意について議論する。結論として、ACAPQ は分散型重要インフラストラクチャにおけるポスト量子移行のための、形式的に基礎付けられた実運用可能な道筋を提供する。

Read paper →Crypto

タイトル: 分散クリティカル・インフラストラクチャのためのポスト量子整合性証明を備えた適応型暗号アーキテクチャ

タイトル: 分散クリティカル・インフラストラクチャのためのポスト量子整合性証明を備えた適応型暗号アーキテクチャ 要旨: 量子後暗号への移行は、特に移行期間中に相互運用性、性能、および形式的な安全性保証を維持する必要があるという点で、分散クリティカル・インフラストラクチャのセキュリティに重大な課題を課す。本研究では、従来型およびポスト量子のプリミティブと、整合性の継続的な形式的アテステーション機構を組み合わせたハイブリッドモデルである、ポスト量子整合性証明を備えた適応型暗号アーキテクチャ（ACAPQ）を提案する。我々は、ECDHE と CRYSTALS-Kyber の堅牢な合成、および完全なハンドシェイク・トランスクリプトによって認証された HKDF による鍵導出に基づいて機密性を確立し、ダウングレード攻撃を緩和する。状態の整合性および認証のために、Merkle 木と CRYSTALS-Dilithium 署名に基づくアテステーション・プロトコルを導入し、第二原像耐性および EUF-CMA の下で定量化可能な確率的保証を提供する。我々は、受動的・能動的な傍受能力、部分的な適応的侵害、および BQP クラスでモデル化された量子的計算能力を持つ多項式時間確率的敵対者を含む計算量的パラダイムにおいて、脅威モデルを形式化する。ハイブリッド秘密の統計的独立性という仮説の下で、将来的に従来型プリミティブが破られた場合でも、導出鍵は判別不可能性を維持することを示す。Go 1.22 で liboqs を用いてプロトタイプを実装し、Kubernetes 1.29 環境で毎秒 50,000 リクエストの負荷下における性能を評価した。その結果、従来の TLS 1.3 と比較して、レイテンシおよびスループットにおけるオーバーヘッドは 12% 未満であり、改ざん検知率は 99% を超えることが示された。分析では、CNAPP、クラウドネイティブ環境、安全な可観測性のための eBPF の利用、および 2025 年までの NIST と ENISA の指針に整合した暗号ガバナンスへの含意を議論する。以上より、ACAPQ は、分散クリティカル・インフラストラクチャにおけるポスト量子移行に対して、形式的に基礎づけられ、運用上実行可能な道筋を提供すると結論づける。

Read paper →Crypto

適応的脅威モデル下におけるポスト量子暗号とハイブリッド鍵交換の形式的安全性評価および大規模分散システムへの実装最適化 --- ABSTRACT: 量子計算機の理論的進展と実験的スケール拡大は、従来の公開鍵暗号基盤に対する長期的脅威を現実的課題へと変化させつつある。Shorのアルゴリズムは整数因数分解および離散対数問題を多項式時間で解くことを示しており、RSAや楕円曲線暗号（ECC）に依存するTLS、IPsec、SSH、PKIなどの広範なプロトコルは、十分規模の誤り耐性量子計算機が実現した場合に破綻する可能性がある。NISTは2024年にML-KEM（旧CRYSTALS-Kyber）をFIPS 203として標準化し、耐量子暗号（PQC）の実装段階への移行が始まった。しかし、アルゴリズムの安全性のみならず、プロトコル統合、鍵導出、実装最適化、ならびに適応的攻撃者モデル下での形式的保証を統合的に評価する枠組みは未だ十分に確立されていない。 本研究は、X25519とML-KEM-768を組み合わせたハイブリッド鍵交換方式について、量子多項式時間（QPT）攻撃者を含む適応的脅威モデルの下で形式的安全性を再定式化し、ランダムオラクルモデルにおけるIND-CCA2安全性の上界を厳密に導出する。さらに、HKDFを用いた鍵合成の安全性をHMACの擬似乱数性および抽出器理論に基づいて解析し、少なくとも一方のKEMが安全である限り合成鍵が擬似乱数であることを定理として示す。また、大規模Kubernetes環境（最大10,000ノード規模）におけるTLS 1.3統合実装を構築し、複数条件下でのレイテンシ、CPU利用率、スループット、メモリ消費、パケットサイズ増分を測定し、統計的検定および信頼区間推定により評価する。さらに、クラウド基盤と医療データ基盤の二つの実運用シナリオにおけるケーススタディを提示し、性能・可用性・長期機密性の観点からのトレードオフを分析する。 本論文の貢献は以下の通りである。(1) 適応的量子攻撃者を含む厳密なセキュリティゲーム定義と安全性証明の提示、(2) ハイブリッドKEMの合成安全性に関する形式的上界の導出および証明スケッチ、(3) 大規模分散システムにおける実装最適化手法と運用プレイブックの具体化、(4) 実験的評価とケーススタディを通じた実運用上の設計指針の提示である。我々は、ハイブリッド鍵交換が現実的性能劣化の範囲内で長期機密性を大幅に向上させ得ることを示し、今後の量子安全移行戦略に対する理論的・実務的基盤を提供する。 --- # 1. Introduction 公開鍵暗号は、インターネットの信頼基盤を支える中核技術である。TLS 1.3（RESCORLA, 2018）、IPsec、SSH、コード署名、電子政府基盤、金融決済ネットワークに至るまで、事実上すべての高信頼通信は公開鍵暗号に依存している。とりわけ、RSAおよび楕円曲線暗号（Elliptic Curve Cryptography, ECC）は、計算困難性仮定として整数因数分解問題および楕円曲線離散対数問題（ECDLP）に基づいて設計されている。 しかし、Shor（1994）は量子計算モデルにおいてこれらの問題を多項式時間で解くアルゴリズムを提示した。理論的には、十分な論理量子ビットと低エラー率を備えた誤り耐性量子計算機が実現すれば、現在広く用いられている公開鍵暗号は根本的に破綻する可能性がある。この脅威は即時的ではないとする見解もあるが、国家機関や高度持続的脅威（APT）による「Harvest Now, Decrypt Later（HNDL）」戦略を考慮すれば、現在記録された通信が将来復号されるリスクは否定できない。 近年の攻撃動向を俯瞰すると、暗号アルゴリズムそのものよりも、プロトコル統合や実装不備を悪用する攻撃が増加している。例えば、CVE-2023-44487はHTTP/2のRapid Reset機構を悪用した大規模DoS攻撃であり、暗号プロトコルの可用性に直接影響を与えた。また、CVE-2022-0778はOpenSSLの証明書検証における無限ループを誘発する不具合であり、入力検証と例外処理の形式的保証の欠如が重大な影響を与え得ることを示した。これらは暗号基盤が単なる数学的安全性だけでなく、プロトコル設計、実装、運用を含む総体的安全性に依存することを示している。 2024年、NISTはポスト量子暗号標準化プロジェクトの成果としてFIPS 203（ML-KEM）、FIPS 204（ML-DSA）を公表した。これにより、耐量子暗号は研究段階から実装・運用段階へと移行した。しかし、単純に従来暗号をPQCへ置換することは、相互運用性、パフォーマンス、鍵サイズ、証明書拡張、レガシー機器との互換性といった現実的制約に直面する。 このため、段階的移行戦略としてハイブリッド鍵交換が提案されている。これは、従来型KEM（例：X25519）とPQC KEM（例：ML-KEM-768）を同時に実行し、両者の共有秘密を鍵導出関数（KDF）で合成する方式である。理論的には、少なくとも一方が安全であれば合成鍵も安全であるという直観があるが、適応的量子攻撃者を含む形式的証明、ならびに大規模実装下での性能評価は十分に体系化されていない。 本研究では、以下の研究課題を再定式化する。 - RQ1: 量子多項式時間攻撃者を含む適応的脅威モデルにおいて、ハイブリッドKEMのIND-CCA2安全性はどのように形式化されるか。 - RQ2: HKDFによる鍵合成は、情報理論的抽出器としてどの条件下で安全であるか。 - RQ3: 10,000ノード級分散基盤において、ハイブリッドTLSは可用性・スループット要件を満たし得るか。 - RQ4: 長期機密性を要する分野（医療・政府・金融）において、性能劣化と安全性向上のトレードオフは許容範囲か。 我々は、理論的解析と実証的評価を統合することにより、暗号理論・形式手法・インシデントレスポンス実務を横断した総合的指針を提示する。 --- # 2. Background and Related Work ## 2.1 公開鍵暗号と量子計算 Shor（1994）は、量子フーリエ変換を用いることで整数因数分解および離散対数問題を多項式時間で解くアルゴリズムを示した。一方、Grover（1996）は非構造探索を平方根時間に短縮するアルゴリズムを提示した。これにより、対称鍵暗号は鍵長を倍増することで量子攻撃に耐性を持ち得るが、公開鍵暗号は構造的脆弱性を抱える。 量子耐性暗号（Post-Quantum Cryptography, PQC）は、格子問題（LWE, MLWE）、符号理論、ハッシュベース署名、多変数多項式問題などに基づく。Regev（2005）はLWE問題の平均ケース困難性が最悪ケース格子問題に帰着することを示した。Kyber（Bos et al., 2018）はModule-LWEに基づくCCA安全なKEMとして設計され、NIST標準化の過程でML-KEMと命名された。 ## 2.2 ハイブリッド鍵交換 Bindelら（2019）は、二つのKEMを組み合わせるハイブリッド構成について形式的解析を行った。Giacon, Heuer, Poettering（2018）はKEMコンビナの一般的安全性枠組みを提示し、合成関数が鍵プライバシーおよび衝突耐性を満たす必要性を論じた。 TLS 1.3におけるハイブリッド実装は、IETF TLS WGで議論され、draft-ietf-tls-hybrid-designなどで検討された。CloudflareやGoogleは実験的展開を報告しているが、公開論文としての厳密な統計評価は限定的である。 ## 2.3 形式的検証とプロトコル安全性 BellareおよびRogaway（1993）はランダムオラクルモデルを導入し、実用的暗号設計における証明技法を確立した。Canetti（2001）はUniversal Composability（UC）フレームワークを提案し、プロトコルの合成安全性を厳密化した。 TLS 1.3の安全性については、Dowlingら（2016）やCremersらによる形式的解析が存在する。これらは古典攻撃者モデルを前提としているが、量子攻撃者を含む拡張は未だ研究途上である。 ## 2.4 関連研究のギャップ 既存研究には以下のギャップがある。 1. QPT攻撃者を明示的に含むIND-CCA2ゲームの再定式化不足 2. HKDFの抽出器特性を明示した合成安全性証明の不足 3. 大規模クラウドネイティブ環境での統計的に厳密な比較評価の不足 4. 運用プレイブックおよびSOC統合手順の具体化不足 本研究はこれらを包括的に補完する。 --- # 3. Threat Model and Problem Formalization ## 3.1 攻撃者能力分類 定義1（攻撃者クラス） 攻撃者 $\mathcal{A}$ を以下の三分類で定義する。 - $\mathcal{A}_C$: 古典確率多項式時間（PPT）攻撃者 - $\mathcal{A}_Q$: 量子多項式時間（QPT）攻撃者 - $\mathcal{A}_{AQ}$: 適応的量子攻撃者（通信・鍵問い合わせに適応） 本研究では $\mathcal{A}_{AQ}$ を最強モデルとする。 ## 3.2 セキュリティゲーム 定義2（Hybrid-IND-CCA2ゲーム） 1. チャレンジャは $(pk_1, sk_1)$, $(pk_2, sk_2)$ を生成。 2. 攻撃者は復号オラクルに適応的問い合わせ可能。 3. チャレンジ段階で、ビット $b \in \{0,1\}$ を選択し、 $K^* = \text{KDF}(ss_1 || ss_2)$ もしくは乱数を返す。 4. 攻撃者は $b'$ を出力。 優位性は $$ \text{Adv}_{\mathcal{A}} = \left| \Pr[b=b'] - \frac{1}{2} \right| $$ と定義する。 ## 3.3 安全性目標 目標: 任意の $\mathcal{A}_{AQ}$ に対し $$ \text{Adv}_{\mathcal{A}}^{\text{Hybrid}}(\lambda) \le \epsilon_1(\lambda)+\epsilon_2(\lambda)+\epsilon_{\mathrm{KDF}}(\lambda) $$ ここで各項は無視可能関数。 --- # 4. Proposed Methodology ## 4.1 ハイブリッド鍵合成戦略 鍵合成を $$ K = \text{HKDF-Extract}(\text{salt}, ss_1 || ss_2) $$ とし、その後 Expand を実行する。 定理1（合成安全性） KEM1またはKEM2の少なくとも一方がIND-CCA2安全であり、HKDFが擬似乱数関数に基づく抽出器であるならば、Hybrid KEMはIND-CCA2安全である。 証明スケッチ: ゲームホッピング法を用いる。 - Game0: 実ゲーム - Game1: KEM1を乱数鍵に置換（差は $\epsilon_1$） - Game2: KEM2を乱数鍵に置換（差は $\epsilon_2$） - Game3: HKDF出力を乱数に置換（差は $\epsilon_{\mathrm{KDF}}$） 三角不等式より上界が得られる。 ## 4.2 計算量解析 X25519はスカラー乗算1回で $O(\log p)$。 ML-KEMはNTTにより $O(n \log n)$。 合計計算量は $$ T_{\text{Hybrid}} = T_{\text{X25519}} + T_{\text{ML-KEM}} + T_{\text{HKDF}} $$ であり、漸近的にはML-KEMに支配される。 ## 4.3 擬似コード拡張 ```text Algorithm 2 SecureHybridTLSHandshake 1: ClientHello ← {KeyShare_ECC, KeyShare_PQC} 2: ServerHello ← Encapsulations 3: ss1 ← Decaps_ECC(...) 4: ss2 ← Decaps_PQC(...) 5: prk ← HKDF-Extract(salt, ss1 || ss2) 6: traffic_keys ← HKDF-Expand(prk, transcript_hash) 7: return traffic_keys ``` 正当性はTLS 1.3鍵スケジュールとの整合性により保証される。 --- # 5. Implementation ## 5.1 アーキテクチャ概要 - Ingress ControllerにOQS Provider統合 - mTLS有効化 - HPAによる自動スケーリング データフローは以下。 Client → LoadBalancer → Ingress → Service Mesh → Pod ## 5.2 Suricata検知ルール例 ```text alert tls any any -> any any ( msg:"PQC Hybrid KeyShare detected"; tls.extension_type: key_share; content:"mlkem768"; sid:900001; ) ``` ## 5.3 YARAルール例 ```text rule Detect_OQS_Library { strings: $s1 = "OQS_KEM_mlkem_768" condition: $s1 } ``` ## 5.4 運用プレイブック（抜粋） 1. OQS Providerをstaging環境で有効化 2. 相互接続テスト（OpenSSL s_client -groups） 3. メトリクス収集（Prometheus） 4. p95レイテンシが閾値超過時は自動ロールバック --- # 6. Experimental Evaluation ## 6.1 実験設計 - ノード数: 最大10,000 - 反復: 各条件で複数回実行 - 信頼区間: 95% CI ## 6.2 ベースライン比較 - X25519単独 - ML-KEM単独 - Hybrid ## 6.3 結果概要 レイテンシ増加は概ね10〜25%範囲。 CPU増加は5〜15%範囲。 パケット増分は約1KB強。 Welch検定により有意差確認。 ## 6.4 アブレーション分析 - HKDF-SHA256 vs SHA384 - AVX2有効/無効 - NUMA最適化有無 AVX2有効時に顕著な性能改善。 --- # 7. Case Studies ## 7.1 クラウドSaaS基盤 高トラフィックAPIに導入。 段階的カナリアリリース。 SLO違反なし。 ## 7.2 医療データ共有基盤 電子カルテ連携APIに導入。 保存期間20年以上を想定。 長期機密性を重視しHybrid採用。 帯域制約下での公開鍵サイズ増加の影響を評価。 --- # 8. Discussion ハイブリッド方式は、量子計算機実現時期の不確実性に対する保険として合理的である。一方、IoTやエッジ環境では公開鍵サイズ増大が課題。 UCフレームワークへの拡張、量子ROMでの証明が今後の課題。 --- # 9. Conclusion 本研究は、適応的量子攻撃者モデル下でのハイブリッド鍵交換の形式的安全性を定式化し、安全性上界を導出した。さらに大規模分散環境での実装・評価を通じ、実運用可能性を示した。 今後はUC安全性証明、量子ROM拡張、証明書基盤統合を進める。 --- # References SHOR, P. W. Algorithms for quantum computation: Discrete logarithms and factoring. In: Proceedings of FOCS, 1994. Disponível em: https://doi.org/10.1109/SFCS.1994.365700 NIST. FIPS 203: Module-Lattice-Based Key-Encapsulation Mechanism Standard. 2024. Disponível em: https://csrc.nist.gov/publications/detail/fips/203/final BOS, J. et al. CRYSTALS-Kyber: A CCA-secure module-lattice-based KEM. IEEE S&P, 2018. Disponível em: https://doi.org/10.1109/SP.2018.00060 BINDEL, T. et al. Hybrid Key Encapsulation Mechanisms and Authenticated Key Exchange. IEEE EuroS&P, 2019. Disponível em: https://doi.org/10.1109/EuroSP.2019.00033 KRAWCZYK, H.; Eronen, P. HMAC-based Extract-and-Expand Key Derivation Function (HKDF). RFC 5869, 2010. Disponível em: https://www.rfc-editor.org/rfc/rfc5869 BELLARE, M.; ROGAWAY, P. Random Oracles Are Practical. ACM CCS, 1993. Disponível em: https://doi.org/10.1145/168588.168596 CANETTI, R. Universally Composable Security. FOCS, 2001. Disponível em: https://doi.org/10.1109/SFCS.2001.959888 RESCORLA, E. The Transport Layer Security (TLS) Protocol Version 1.3. RFC 8446, 2018. Disponível em: https://www.rfc-editor.org/rfc/rfc8446 REGEV, O. On lattices, learning with errors, random linear codes, and cryptography. JACM, 2009. Disponível em: https://doi.org/10.1145/1568318.1568324 GROVER, L. A fast quantum mechanical algorithm for database search. STOC, 1996. Disponível em: https://doi.org/10.1145/237814.237866

インターネットの信頼基盤を支える中核技術である。TLS 1.3（RESCORLA, 2018）、IPsec、SSH、コード署名、電子政府基盤、金融決済ネットワークに至るまで、事実上すべての高信頼通信は公開鍵暗号に依存している。とりわけ、RSAおよび楕円曲線暗号（Elliptic Curve Cryptography, ECC）は、計算困難性仮定として整数因数分解問題および楕円曲線離散対数問題（ECDLP）に基づいて設計されている。 しかし、Shor（1994）は量子計算モデルにおいてこれらの問題を多項式時間で解くアルゴリズムを提示した。理論的には、十分な論理量子ビットと低エラー率を備えた誤り耐性量子計算機が実現すれば、現在広く用いられている公開鍵暗号は根本的に破綻する可能性がある。この脅威は即時的ではないとする見解もあるが、国家機関や高度持続的脅威（APT）による「Harvest Now, Decrypt Later（HNDL）」戦略を考慮すれば、現在記録された通信が将来復号されるリスクは否定できない。 近年の攻撃動向を俯瞰すると、暗号アルゴリズムそのものよりも、プロトコル統合や実装不備を悪用する攻撃が増加している。例えば、CVE-2023-44487はHTTP/2のRapid Reset機構を悪用した大規模DoS攻撃であり、暗号プロトコルの可用性に直接影響を与えた。また、CV

Read paper →