LLM による形式的セキュリティプロトコル解析の評価──推論モデルは精度 66.5% に達するも攻撃検知は 5 割未満

論文概要

本研究では、ProVerif や OFMC といった形式的検証ツールに対し、大規模言語モデル（LLM）が同等のセキュリティプロトコル解析を実施できるかを評価している。GPT および DeepSeek のチャットモードおよび推論モードを使用し、3 実行にわたって 130 件の難読化された AnB/AnBx プロトコル（388 件のセキュリティ目標を含む）をテストした結果、チャットモデルは再現率 69〜81% を記録する一方で適合率は 31% 未満に留まり、推論モデルは適合率を GPT で 66.5%、DeepSeek で 45.4% まで高める代わりに攻撃検知率が半数強に低下するというトレードオフを明らかにしている。

関連研究

セキュリティプロトコルの検証は、従来 ProVerif や OFMC などの形式的手法ツールに大きく依存してきた。これらは厳密な数学的保証を提供する反面、モデル化のコストや大規模プロトコルにおける状態爆発の問題を抱える。近年の LLM のコード解析や推論能力の向上に伴い、脆弱性検出への適用が模索されているが、シンボリックなセキュリティプロトコル解析における定量的な実力評価はこれまで十分に行われていなかった。

新規性と貢献

本研究の最大の貢献は、LLM のチャットモードと推論モードにおける解析能力のトレードオフを、130 件の難読化プロトコルと 388 件のセキュリティ目標に基づく大規模なベンチマークで定量的に示した点にある。特に DeepSeek の同一基盤モデルにおける 2 つのモード比較により、純粋な推論機能が適合率を 27.2% から 45.4% へ向上させる効果を明確に切り離して検証した点が学術的・実用的な価値を持つ。

提案手法の詳細

評価には、Dolev-Yao 侵入者モデルに基づく難読化された AnB/AnBx プロトコルを使用し、チャットモデルと推論モデルの挙動を比較した。推論モードでは思考プロセスを挟むことで誤検知を抑制し、適合率の向上を図っている。一方、認証目標などの複雑な検証においては、単なるトークン処理や推論の拡張だけでは不十分であり、形式的検証ツールの補完としてどのような構造が必要かという設計上の課題を浮き彫りにしている。

評価・考察

評価結果として、チャットモデルは 69 から 81% の再現率を記録したが、適合率は 31% 未満であった。推論モデルはこのトレードオフを逆転させ、GPT で 66.5%、DeepSeek で 45.4% の適合率を達成したものの、攻撃の検出は半数強に留まった。目標別では機密性（Confidentiality）において推論モードの F1 スコアが最大 95.7% と非常に高い精度を示した一方、認証目標（Authentication）では著しく性能が低下し、推論モデルでも合意攻撃の検知は半数未満であった。 また、判定結果の実行間安定性は GPT で目標の 89.7%、DeepSeek で 74.0% とモデル間でばらつきがあり、自己申告の信頼度は一様に高いにもかかわらず正解率との相関が全く見られない点が指摘されている。

応用例と今後の展望

本研究の結果から、現行の LLM は形式的検証ツールを完全に代替することはできず、せいぜい事前スクリーニングフィルタとしての活用にとどまることが示されている。金融・決済システムやクラウドインフラ等のセキュリティプロトコル設計を行う国内のセキュリティエンジニアや研究者にとって、LLM を脆弱性検出パイプラインに組み込む際は誤検知や認証目標の見落としリスクを前提とした二重チェック体制が不可欠となる。

結論

LLM はシンボリックなセキュリティプロトコル解析において、機密性評価など一部の領域で高い性能を示すものの、認証関連の脆弱性検出や判定の安定性には深刻な限界が存在する。現時点では完全な形式的検証の代替ではなく、限定的なプレスクリーニングとしての運用が限界であると結論づけられている。

注釈

• ProVerif / OFMC: セキュリティプロトコルの自動検証を行う代表的な形式的検証ツール。
• AnB/AnBx: セキュリティプロトコルを記述するための抽象言語（Alice-Bob notation の一種）。
• Dolev-Yao 模型: 暗号プロトコル解析において、通信路を完全に支配する強力な攻撃者を仮定する標準的な脅威モデル。