論文の概要: LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?

• arxiv url: http://arxiv.org/abs/2609.35434v1
• Date: Mon, 28 Sep 2026 15:38:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-02 05:28:27.414901
• Title: LLM-Assisted Automatic Security Proofs for Cryptographic Protocols: How Far Are We?
• Title（参考訳）: LLMによる暗号化プロトコルの自動セキュリティ証明:どこまで遠いか?
• Abstract要約: 大規模言語モデル(LLM)は、ソフトウェアやセキュリティ分析タスクを支援する強力な可能性を示している。 我々は,暗号シンボルプロトコル検証における最先端LLMの能力について,最初の体系的評価を行った。
• 参考スコア（独自算出の注目度）: 10.263102436832293
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Large language models (LLMs) have shown strong potential for assisting software and security analysis tasks, yet their effectiveness in cryptographic symbolic protocol verification remains insufficiently understood. In this paper, we conduct the first systematic evaluation of the capability of state-of-the-art LLMs in cryptographic symbolic protocol verification. To quantify this capability, we propose \textsc{CRoST} (Coverage Rate of Solve Tree), a proof-based metric derived from the verifier's proof skeleton that measures the similarity between generated lemmas and reference lemmas. We then establish the rationale of \textsc{CRoST} through both theoretical analysis and empirical validation. The evaluation results show that state-of-the-art models achieve 38.82\% coverage on average, with 14.4\% of generated lemmas exceeding 80\% coverage, indicating that LLMs can already generate useful lemmas to a certain extent. However, they still exhibit non-trivial failure modes on complex multi-phase protocols, show diminishing returns under naive scaling, and incur substantial verification overhead. These findings clarify the practical potential and limitations of LLMs for protocol verification and motivate future work on complex real-world protocols.
• Abstract（参考訳）: 大規模言語モデル(LLM)は、ソフトウェアやセキュリティ分析タスクを補助する強力な可能性を示しているが、暗号記号プロトコル検証におけるその有効性はまだ十分に理解されていない。 本稿では,暗号シンボルプロトコル検証における最先端LLMの能力について,最初の体系的評価を行う。 この能力を定量化するために、検証者の証明骨格から導かれる証明に基づく計量である「textsc{CRoST} (Coverage Rate of Solve Tree)」を提案し、生成した補題と参照補題の類似性を測定する。 次に, 理論的解析と実証的検証の両面から, textsc{CRoST} の理論的根拠を確立する。 評価結果から, 最先端モデルでは平均38.82 %, 生成したレムマの14.4 %が80 %を超え, LLM が既にある程度有用なレムマを生成可能であることが示された。 しかし、複雑なマルチフェーズプロトコルに非自明な障害モードを示し、単純なスケーリングの下でリターンが低下し、かなりの検証オーバーヘッドが生じる。 これらの結果から,LLMの実用的可能性と限界が明らかとなり,複雑な実世界のプロトコルに対する今後の取り組みを動機付けている。

関連論文リスト

• Integrated and Cross-Architecture Interpretation of LLM Reasoning [48.58940522466915]
  統合されたクロスアーキテクチャ推論(IAR)フレームワークは、LLM推論の解釈可能性に対する統一的なアプローチを提供するように設計されている。 まず、チューキーIQRピーク検出と組み合わされた帯域幅校正MIPを用いて、出力層における推論・クラシカルトークンを分離することを提案する。 次に、MIP-pickedトークンと計算深度トークンの重なり解析を行い、それらのトークンの層間軌跡をトレースする。
  論文  参考訳（メタデータ） (2026-05-27T05:56:35Z)
• Neuro-Symbolic Verification of LLM Outputs for Data-Sensitive Domains (extended preprint) [0.08594140167290099]
  本稿では,形式的記号法とニューラルセマンティック解析を組み合わせたハイブリッド検証アーキテクチャを提案する。 出力検証のために、埋め込みに基づく意味的類似性はコンテキスト幻覚を検出する。 評価の結果, 構造体では83%, 意味形成では72%以上の幻覚検出率を示した。
  論文  参考訳（メタデータ） (2026-05-26T12:32:17Z)
• Reasoning with Confidence: Efficient Verification of LLM Reasoning Steps via Uncertainty Heads [104.9566359759396]
  データ駆動の不確実性スコアに基づくステップレベルの推論検証の軽量な代替案を提案する。 本研究は, LLMの内部状態が不確実性を符号化し, 信頼性の高い検証信号として機能することが示唆された。
  論文  参考訳（メタデータ） (2025-11-09T03:38:29Z)
• Beyond Next Token Probabilities: Learnable, Fast Detection of Hallucinations and Data Contamination on LLM Output Distributions [60.43398881149664]
  LLM出力シグナチャの効率的な符号化を訓練した軽量アテンションベースアーキテクチャであるLOS-Netを紹介する。 非常に低い検出レイテンシを維持しながら、さまざまなベンチマークやLLMで優れたパフォーマンスを実現している。
  論文  参考訳（メタデータ） (2025-03-18T09:04:37Z)
• Detecting LLM Hallucination Through Layer-wise Information Deficiency: Analysis of Ambiguous Prompts and Unanswerable Questions [60.31496362993982]
  大規模言語モデル(LLM)は、自信を持って不正確な応答を頻繁に生成する。 本稿では,情報フローの系統的解析を通じて,モデル幻覚を検出する新しいテストタイム手法を提案する。
  論文  参考訳（メタデータ） (2024-12-13T16:14:49Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Exploring Automatic Cryptographic API Misuse Detection in the Era of LLMs [60.32717556756674]
  本稿では,暗号誤用の検出において,大規模言語モデルを評価するための体系的評価フレームワークを提案する。 11,940個のLCM生成レポートを詳細に分析したところ、LSMに固有の不安定性は、報告の半数以上が偽陽性になる可能性があることがわかった。 最適化されたアプローチは、従来の手法を超え、確立されたベンチマークでこれまで知られていなかった誤用を明らかにすることで、90%近い顕著な検出率を達成する。
  論文  参考訳（メタデータ） (2024-07-23T15:31:26Z)
• Token-Level Adversarial Prompt Detection Based on Perplexity Measures and Contextual Information [67.78183175605761]
  大規模言語モデルは、敵の迅速な攻撃に影響を受けやすい。 この脆弱性は、LLMの堅牢性と信頼性に関する重要な懸念を浮き彫りにしている。 トークンレベルで敵のプロンプトを検出するための新しい手法を提案する。
  論文  参考訳（メタデータ） (2023-11-20T03:17:21Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。