論文の概要: Decidability of Parameterised Dolev-Yao Secrecy
- arxiv url: http://arxiv.org/abs/2608.02838v1
- Date: Mon, 03 Aug 2026 19:51:46 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-06 07:04:20.679842
- Title: Decidability of Parameterised Dolev-Yao Secrecy
- Title（参考訳）: パラメタライズドレフ・ヤオ秘密の判定可能性
- Abstract要約: 本研究では,Dolev-Yaoモデルにおける暗号プロトコルのパラメータ化シークレットの検証について検討する。
任意の数のセッションを持つシステムにおける秘密違反は、常に境界サイズのシステムで観測される。
- 参考スコア（独自算出の注目度）: 3.9737423502459106
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: We study the verification of parameterised secrecy for cryptographic protocols in the Dolev-Yao model, where the number of protocol sessions is unbounded and treated as a parameter. This differs fundamentally from classical Dolev-Yao secrecy, which asks whether a protocol leaks a secret irrespective of the number of executions; our question is whether secrecy holds uniformly across all system sizes, where such a size is a parameter. This parameterised perspective captures how attacks scale with the number of participants and provides a formal basis for the empirical effectiveness of small-instance analysis. Secrecy (parameterised or not) is undecidable in general, even under bounded freshness or bounded message size. We identify two structural restrictions that make parameterised secrecy decidable: (i) global bounded freshness per role, and (ii) a Dolev-Yao intruder restricted to well-typed substitutions. Under these assumptions, protocol executions admit a finite representation up to a collapsing map on agents and terms. Our main result is that parameterised secrecy is decidable in this setting. We obtain a cut-off theorem: secrecy violations in systems with arbitrarily many sessions are always witnessed in systems of bounded size. The cut-off is self-contained; more strongly, the induced transition system forms a well-structured transition system (WSTS) under a bound-based ordering, so secrecy also reduces to a coverability problem in WSTS. This provides a structural explanation for the existence of finite witnesses in symbolic protocol analysis and connects Dolev-Yao verification with parameterised verification techniques.
- Abstract（参考訳）: 本研究では,プロトコルセッションの数が無拘束でパラメータとして扱われるDolev-Yaoモデルにおいて,暗号プロトコルのパラメータ化シークレットの検証について検討する。
これは、プロトコルが実行数に関係なく秘密を漏らすかどうかを問う古典的なDolev-Yao Secrecyとは根本的に異なる。
このパラメータ化されたパースペクティブは、参加者数に応じて攻撃がどのようにスケールするかをキャプチャし、小規模インスタンス分析の実証的効果の正式な基盤を提供する。
機密性(パラメータ化されるかしないか)は一般には決定不可能である。
パラメータ化された機密を決定できる2つの構造的制約を特定します。
一 役割ごとの世界的有界新鮮度、及び
(ii) ドレフ・ヤオ侵入者は, 良好な置換に制限された。
これらの仮定の下では、プロトコルの実行はエージェントと項の折り畳みマップまでの有限表現を許容する。
私たちの主な結果は、パラメータ化された機密は、この設定で決定可能であることです。
任意の数のセッションを持つシステムにおける秘密違反は、常に境界サイズのシステムで観測される。
カットオフは自己完結しており、より強くは、誘導遷移系は境界ベースの順序付けの下で十分に構造化された遷移系(WSTS)を形成するため、機密性もWSTSのカバー可能性の問題に還元される。
これは、シンボリックプロトコル解析における有限証人の存在に関する構造的説明を提供し、ドレフ・ヤオ検証とパラメータ化された検証手法を結びつける。
関連論文リスト
- AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
AIスロープ(AI slop)は、アーティファクト、幻覚的脆弱性、可視だが正しくないパッチ、セマンティックに再パッケージされたバグレポートである。
本稿では,実証的証拠を調査し,統一メカニズムを特定し,信頼に値するトリアージへの道筋をたどる。
論文 参考訳（メタデータ） (2026-08-26T11:48:38Z) - Logit-Boundary Geometric Belief Interfaces and Sparse Sheaf-Enclave Protocols: A Self-Contained Substrate for Secure Network Electronic Health Record (EHR) Interoperability [2.894286977279531]
本稿では,そのインターフェースの数学的および工学的アーキテクチャについて詳述する。
発見モデルは、局所的なカテゴリー決定よりも事前閾値スコアを提案するが、決定論的判断基盤は、提案が許容できるかどうかを決定する。
得られたGeometric Belief Interface(GBI)は、有限境界セマンティクス、ローカルディリクレのエビデンス、セルラーシェーフとマッピングコーンの診断、アドバイザリ監査チャート、フェールクローズドデプロイメントのための分散暗号化シーフ-エンクレーブプロトコルスケッチを組み合わせたものである。
論文 参考訳（メタデータ） (2026-08-10T23:10:53Z) - Constraint-Driven Synthesis of Hyper Petri Nets [46.9047309711542]
本稿では,ペトリネット(PN)を用いた制約ロボットシステムのモデリングと合成について述べる。
全ての可観測系状態が与えられた論理的制約を満たしつつ、実行可能な遷移意味論と整合性を維持したモデルを構築する方法について検討する。
提案手法では,観測可能な状態に対する明示的な実行セマンティクスを導入する。
論文 参考訳（メタデータ） (2026-07-24T07:57:19Z) - LeanDY: Type-Based and Trace-Based Symbolic Protocol Verification in Lean [9.293322518056357]
本稿では,タイプベースの推論とトレースベースの推論を組み合わせることで,ステートフルプロトコルとアンバウンドプロトコルのモジュール検証を実現する手法を提案する。
私たちはこのフレームワークをリーン実証アシスタント用のLeanDYライブラリとして実装し、DY*の設計を構築し拡張します。
我々は、LeanDYでSegWitスタイルのブロックチェーンプリミティブを形式化し、支払いチャネルの詳細な形式化を行うことで、その表現性を実証する。
論文 参考訳（メタデータ） (2026-07-03T15:12:30Z) - Compiling Activation Steering into Weights via Null-Space Constraints for Stealthy Backdoors [48.881343993730844]
安全性に整合した大規模言語モデル(LLM)は、現実世界のパイプラインにますますデプロイされている。
敵は通常の評価では動作しないバックドアのチェックポイントを配布することができる。
最近のポストホック重み付け法は、そのようなバックドアを注入するための効率的なアプローチを提供する。
論文 参考訳（メタデータ） (2026-04-14T06:48:33Z) - AlignSAE: Concept-Aligned Sparse Autoencoders [47.18866175760984]
本稿では,SAE の機能と定義オントロジーを"pre-train, then-train" カリキュラムで整合させる手法である AlignSAE を紹介する。
初期教師なしトレーニングフェーズの後、特定の概念を専用潜在スロットにバインドするために教師付きポストトレーニングを適用する。
この分離により、非関係な特徴から干渉することなく、特定の関係を検査・制御できる解釈可能なインターフェースが生成される。
論文 参考訳（メタデータ） (2025-12-01T18:58:22Z) - Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。
以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。
我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
論文 参考訳（メタデータ） (2025-08-26T20:59:16Z) - Invariant-Based Cryptography [0.0]
Schemeは、制御されたパラメータ化の下で保存された4点代数的アイデンティティを通じて秘密整数を符号化する。
我々は、完全な分析およびモジュラーフレームワークを開発し、正確なアイデンティティを証明し、インデックス回復手順を定義し、セキュリティ仮定を分析する。
論文 参考訳（メタデータ） (2025-05-08T21:18:59Z) - Is Vertical Logistic Regression Privacy-Preserving? A Comprehensive
Privacy Analysis and Beyond [57.10914865054868]
垂直ロジスティック回帰(VLR)をミニバッチ降下勾配で訓練した。
我々は、オープンソースのフェデレーション学習フレームワークのクラスにおいて、VLRの包括的で厳密なプライバシー分析を提供する。
論文 参考訳（メタデータ） (2022-07-19T05:47:30Z) - Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
完全同型暗号方式として, 完全同型暗号方式を初めて構築する。
我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
論文 参考訳（メタデータ） (2022-03-03T10:07:32Z) - Sharing classical secrets with continuous-variable entanglement:
Composable security and network coding advantage [0.913755431537592]
量子通信のためのポイント・ツー・ポイントプロトコルに対して,マルチパーティ・エンタングルド・リソースが真に有利であることを示す。
これは、量子通信のためのポイント・ツー・ポイントプロトコルよりも真に有利な、マルチパーティ・エンタングルド・リソースの最初の具体的な例である。
論文 参考訳（メタデータ） (2021-04-21T17:37:28Z) - SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
パラメータ化マルチエージェントシステム(MAS)の検証について検討する。
特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
論文 参考訳（メタデータ） (2020-08-11T15:24:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。