論文の概要: Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
- arxiv url: http://arxiv.org/abs/2608.22954v1
- Date: Mon, 24 Aug 2026 08:19:26 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-25 13:29:43.964251
- Title: Rational Dolev--Yao Attackers: Decidable Incentive-Aware Verification of Security Protocols in Strategic Logic
- Title(参考訳): Rational Dolev--Yao攻撃者: 戦略論理におけるセキュリティプロトコルの決定可能なインセンティブ-アウェア検証
- Abstract要約: 我々は,有限コストの同時ゲーム構造に対して有界な有理DY侵入に対して決定可能であることを証明した。
いくつかのプロトコルはDY非セキュアだが合理的に安全であり、計算可能なしきい値によって分離される。
- 参考スコア(独自算出の注目度): 2.2889059978882624
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Symbolic protocol verification models the network attacker as a Dolev--Yao (DY) intruder, which does everything its knowledge permits, whether or not it serves any purpose; real adversaries instead maximise utility, attacking only when the payoff is positive. We introduce a rational Dolev--Yao attacker, a DY intruder whose actions carry costs and whose security-violating goals carry rewards, and call a protocol rationally secure when no intruder strategy achieves a violation with strictly positive utility, expressed in a weighted fragment of ATL (WATL). We prove this decidable for a bounded rational DY intruder over a finite cost-annotated concurrent game structure, characterise its complexity, and show it strictly refines DY security: some protocols are DY-insecure yet rationally secure, separated by a computable threshold. We illustrate the framework on two contrasting use-cases: an authenticated payment under session uncertainty, where a rational intruder must strategise across indistinguishable sessions and its imperfect information strictly raises the attack cost a designer must price against; and ThreeBallot, a cryptography-free scheme where we pinpoint the bribe-to-benefit ratio below which no rational coercer attacks.
- Abstract(参考訳): シンボリックプロトコル検証は、ネットワーク攻撃者をDolev-Yao(DY)侵入者としてモデル化する。これは、その知識が何らかの目的を果たすか否かに関わらず、全てを許容する。実際の敵はユーティリティを最大化し、支払いがポジティブな場合にのみ攻撃する。我々は、コストを負担する合理的なDY侵入者であるDolev-Yao攻撃者を導入し、攻撃者戦略がATL(WATL)の重み付きフラグメントで表現された厳密な正効性に違反した場合、プロトコルを合理的に保護する。
有限のコストアノテートされた並列ゲーム構造に対して有界な有理なDY侵入者に対して決定可能であることを証明し、その複雑さを特徴付け、DYセキュリティを厳密に洗練することを示す。
セッションの不確実性の下での認証支払いでは、合理的侵入者が識別不可能なセッションをまたいでストラテジケートし、その不完全な情報がデザイナーが価格を下げなければならない攻撃コストを厳密に引き上げなければならない。
関連論文リスト
- Fair ASR: Re-Evaluating Black-Box Jailbreaks under Shared Target-Call Budgets [18.83088278144739]
本稿では,ブラックボックス・ジェイルブレイク攻撃の評価プロトコルであるFair-ASRを紹介する。
我々は、Fair-ASRプロトコルの下での11の代表的な攻撃を再評価し、攻撃ランクがターゲットコール予算によって大きく変わることを発見した。
この効率ギャップに動機づけられたReCodeは、デセンシタイズ書き換えと2つの効果的な低コストプリミティブを組み合わせた構成的予算効率の攻撃である。
論文 参考訳(メタデータ) (2026-08-18T04:26:39Z) - Analyzing Defensive Misdirection Against Model-Guided Automated Attacks on Agentic AI Systems [0.0]
エージェントAIシステムは、命令を解釈し、外部データを処理し、ツールを呼び出し、他のエージェントと調整するための言語モデルコンポーネントにますます依存している。
本研究は、標的システムの確率モデル、防御機構、および攻撃者の自動判断による攻撃防御設定を解析する。
論文 参考訳(メタデータ) (2026-06-18T16:50:28Z) - TwinGate: Stateful Defense against Decompositional Jailbreaks in Untraceable Traffic via Asymmetric Contrastive Learning [60.68349524623048]
分解されたジェイルブレイクは、大きな言語モデルにとって重大な脅威となる。
我々はステートフルなデュアルエンコーダ防御フレームワークであるTwinGateを紹介する。
我々は、8600の異なる悪意のある意図にまたがる360万以上の命令の包括的なデータセットを構築した。
論文 参考訳(メタデータ) (2026-04-30T13:44:01Z) - Prompt-Unknown Promotion Attacks against LLM-based Sequential Recommender Systems [51.504307822017985]
大規模言語モデルを用いたシーケンシャルレコメンデータシステム(LLM-SRS)は,最近顕著な性能を示した。
本稿では, LLM-SRSにおけるアイテムプロモーション攻撃について, 攻撃者に対してシステムプロンプトと被害者モデルの両方が未知な状況下で, より現実的な状況下で検討する。
論文 参考訳(メタデータ) (2026-04-26T10:09:26Z) - TraceGuard: Process-Guided Firewall against Reasoning Backdoors in Large Language Models [19.148124494194317]
我々は,小規模モデルを堅牢な推論ファイアウォールに変換するプロセス誘導型セキュリティフレームワークであるTraceGuardを提案する。
提案手法は,推理トレースを信頼できないペイロードとして扱い,詳細な防衛戦略を確立する。
グレーボックス設定における適応的敵に対する堅牢性を実証し、TraceGuardを実用的で低レイテンシなセキュリティプリミティブとして確立する。
論文 参考訳(メタデータ) (2026-03-02T22:19:13Z) - CausalArmor: Efficient Indirect Prompt Injection Guardrails via Causal Attribution [49.689452243966315]
ツールコール機能を備えたAIエージェントは、IPI(Indirect Prompt Injection)攻撃の影響を受けやすい。
本稿では,選択防衛フレームワークCausalArmorを提案する。
AgentDojoとDoomArenaの実験は、CausalArmorが攻撃的な防御のセキュリティと一致することを示した。
論文 参考訳(メタデータ) (2026-02-08T11:34:08Z) - SafeThinker: Reasoning about Risk to Deepen Safety Beyond Shallow Alignment [43.86865924673546]
軽量なゲートウェイ分類器を介して防御資源を割り当てる適応型フレームワークであるSafeThinkerを提案する。
実験によると、SafeThinkerは、堅牢性を損なうことなく、さまざまなジェイルブレイク戦略における攻撃の成功率を大幅に低下させる。
論文 参考訳(メタデータ) (2026-01-23T07:12:53Z) - Cognitive Control Architecture (CCA): A Lifecycle Supervision Framework for Robustly Aligned AI Agents [1.014002853673217]
LLMエージェントはIPI(Indirect Prompt Injection)攻撃に対して脆弱である。
IPIは外部情報ソースを汚染することでハイジャックエージェントの動作を攻撃している。
本稿では,全ライフサイクルの認知管理を実現するための総合的な枠組みである認知制御アーキテクチャ(CCA)を提案する。
論文 参考訳(メタデータ) (2025-12-07T08:11:19Z) - ARMOR: Aligning Secure and Safe Large Language Models via Meticulous Reasoning [64.32925552574115]
ARMORは、jailbreak戦略を分析し、コアインテントを抽出する、大規模な言語モデルである。
ARMORは最先端の安全性能を達成し、平均有害率は0.002であり、高度な最適化ベースのジェイルブレイクに対する攻撃成功率は0.06である。
論文 参考訳(メタデータ) (2025-07-14T09:05:54Z) - Benchmarking Misuse Mitigation Against Covert Adversaries [80.74502950627736]
既存の言語モデルの安全性評価は、オーバースト攻撃と低レベルのタスクに重点を置いている。
我々は、隠蔽攻撃と対応する防御の評価を自動化するデータ生成パイプラインである、ステートフルディフェンスのためのベンチマーク(BSD)を開発した。
評価の結果,分解攻撃は有効な誤用防止剤であり,その対策としてステートフルディフェンスを強調した。
論文 参考訳(メタデータ) (2025-06-06T17:33:33Z) - Effective Targeted Attacks for Adversarial Self-Supervised Learning [58.14233572578723]
ラベル情報を持たないモデルにおいて堅牢性を達成する手段として、教師なしの敵訓練(AT)が強調されている。
本稿では,敵のSSLフレームワークを効果的に生成するために,敵の攻撃を標的とした新たな正のマイニングを提案する。
提案手法は,非コントラスト型SSLフレームワークに適用した場合のロバストネスの大幅な向上と,コントラスト型SSLフレームワークによるロバストネスの向上を示す。
論文 参考訳(メタデータ) (2022-10-19T11:43:39Z) - Adversarial Visual Robustness by Causal Intervention [56.766342028800445]
敵の訓練は、敵の例に対する事実上最も有望な防御である。
しかし、その受動性は必然的に未知の攻撃者への免疫を妨げる。
我々は、敵対的脆弱性の因果的視点を提供する: 原因は、学習に普遍的に存在する共同創設者である。
論文 参考訳(メタデータ) (2021-06-17T14:23:54Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。