論文の概要: Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling

• arxiv url: http://arxiv.org/abs/2609.37396v1
• Date: Tue, 29 Sep 2026 12:41:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-30 21:28:47.492062
• Title: Confidence-Guided Protocol IR for LLM-Aided Security Protocol Modeling
• Title（参考訳）: LLM支援セキュリティプロトコルモデリングのための信頼誘導プロトコルIR
• Abstract要約: 本稿では,セキュリティプロトコルの形式モデルを生成するためのヒューマン・イン・ザ・ループ・フレームワークを提案する。 我々のキーとなる観察は、中間プロトコル表現の構文的妥当性よりも意味論的精度が主な正当性ボトルネックであるということである。
• 参考スコア（独自算出の注目度）: 13.676279821923009
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models offer a promising interface for translating natural-language protocol descriptions into formal security models, but their outputs remain difficult to trust without expert validation. In this paper, we present a human-in-the-loop framework for generating Tamarin-verifiable formal models of security protocols. Our key observation is that the main correctness bottleneck is the semantic accuracy rather than the syntactic validity of the intermediate protocol representation. To address this problem, we introduce a protocol intermediate representation (IR) that serves as a human-auditable semantic checkpoint between natural-language parsing and formal model generation. The IR explicitly captures protocol participants, message flows, value provenance, cryptographic operations, proof targets, and compromise assumptions. We further design an interactive interface that highlights uncertain fields and guides users to inspect the most critical semantic decisions based on model confidence before model generation. Rather than replacing formal-methods experts, our approach uses LLMs to produce auditable semantic drafts while leveraging verification tools to check the resulting formal models. Code and verification artifacts are available at https://github.com/laplace1002/TamarinAgent.git.
• Abstract（参考訳）: 大規模言語モデルは、自然言語プロトコル記述を形式的なセキュリティモデルに変換するための有望なインターフェースを提供するが、その出力は専門家の検証なしには信頼できない。 本稿では,タマリン検証可能なセキュリティプロトコルの形式モデルを生成するためのヒューマン・イン・ザ・ループ・フレームワークを提案する。 我々のキーとなる観察は、中間プロトコル表現の構文的妥当性よりも意味論的精度が主な正当性ボトルネックであるということである。 この問題に対処するために,自然言語解析と形式モデル生成の人間可聴な意味チェックポイントとして機能するプロトコル中間表現(IR)を導入する。 IRは、プロトコル参加者、メッセージフロー、値証明、暗号操作、証明ターゲット、妥協仮定を明示的にキャプチャする。 さらに,不確実性に着目した対話型インタフェースを設計し,モデル生成前のモデル信頼度に基づいて,ユーザが最も重要な意味決定を検査できるように指導する。 フォーマルメソッドの専門家を置き換えるのではなく、我々のアプローチはLCMを使って監査可能なセマンティックドラフトを作成し、検証ツールを活用して結果のフォーマルモデルをチェックする。 コードと検証アーティファクトはhttps://github.com/laplace1002/TamarinAgent.gitで公開されている。

関連論文リスト

• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agentは自然言語の自動形式化と形式モデル修復のためのエンドツーエンドフレームワークである。 これは、大きな言語モデルの生成能力と形式的検証の厳密さを組み合わせたものである。
  論文  参考訳（メタデータ） (2025-09-28T06:32:14Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• ModelForge: Using GenAI to Improve the Development of Security Protocols [1.9241821314180376]
  プロトコル仕様の翻訳を自動化する新しいツールであるModelForgeを紹介する。 自然言語処理(NLP)と生成AI(GenAI)の進歩を活用することで、ModelForgeはプロトコル仕様を処理し、CPSAプロトコル定義を生成する。
  論文  参考訳（メタデータ） (2025-06-08T06:27:09Z)
• Large Language Models for Validating Network Protocol Parsers [8.007994733372675]
  プロトコル標準は一般的に自然言語で書かれるが、実装はソースコードで書かれている。 大規模言語モデル(LLM)に基づくフレームワークであるPARVALを提案する。 プロトコル標準とそれらの実装の両方を、フォーマット仕様と呼ばれる統一された中間表現に変換する。 実装とRFC標準の矛盾をうまく識別し、偽陽性率は5.6%と低い。
  論文  参考訳（メタデータ） (2025-04-18T07:09:56Z)
• Towards Auto-Modeling of Formal Verification for NextG Protocols: A Multimodal cross- and self-attention Large Language Model Approach [3.9155346446573502]
  本稿では,5GおよびNextGプロトコル(AVRE)のための実世界プロンプトを用いた形式検証の自動モデリングを提案する。 AVREは次世代通信プロトコル(NextG)の正式な検証のために設計された新しいシステムである。
  論文  参考訳（メタデータ） (2023-12-28T20:41:24Z)
• FLIP: Fine-grained Alignment between ID-based Models and Pretrained Language Models for CTR Prediction [49.510163437116645]
  クリックスルーレート(CTR)予測は、パーソナライズされたオンラインサービスにおいてコア機能モジュールとして機能する。 CTR予測のための従来のIDベースのモデルは、表形式の1ホットエンコードされたID特徴を入力として取る。 事前訓練された言語モデル(PLM)は、テキストのモダリティの文を入力として取る別のパラダイムを生み出した。 本稿では,CTR予測のためのIDベースモデルと事前学習言語モデル(FLIP)間の細粒度特徴レベルのアライメントを提案する。
  論文  参考訳（メタデータ） (2023-10-30T11:25:03Z)

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

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