論文の概要: Automatic verification of Finite Variant Property beyond convergent equational theories

• arxiv url: http://arxiv.org/abs/2410.15289v1
• Date: Sun, 20 Oct 2024 05:11:30 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-22 13:15:30.951535
• Title: Automatic verification of Finite Variant Property beyond convergent equational theories
• Title（参考訳）: 収束方程式理論を超えた有限変数性の自動検証
• Authors: Vincent Cheval, Caroline Fontaine,
• Abstract要約: セキュリティプロトコルのほとんどの自動検証は、有限変数性(FVP)を満たす方程式理論に焦点を当てている。 本稿では,FVPの特定表現を必要とせずにFVPを証明し,E-convergentリライトシステムによって表現される理論を超越した理論のクラスについて,新たな半決定手順を提案する。
• 参考スコア（独自算出の注目度）: 5.9972628641893015
• License:
• Abstract: Computer-aided analysis of security protocols heavily relies on equational theories to model cryptographic primitives. Most automated verifiers for security protocols focus on equational theories that satisfy the Finite Variant Property (FVP), for which solving unification is decidable. However, they either require to prove FVP by hand or at least to provide a representation as an E-convergent rewrite system, usually E being at most the equational theory for an associative and commutative function symbol (AC). The verifier ProVerif is probably the only exception amongst these tools as it automatically proves FVP without requiring a representation, but on a small class of equational theories. In this work, we propose a novel semi-decision procedure for proving FVP, without the need for a specific representation, and for a class of theories that goes beyond the ones expressed by an E-convergent rewrite system. We implemented a prototype and successfully applied it on several theories from the literature.
• Abstract（参考訳）: セキュリティプロトコルのコンピュータ支援分析は、暗号プリミティブをモデル化するための方程式理論に大きく依存している。 セキュリティプロトコルのほとんどの自動検証は、統一の解決が決定可能なFVP(Finite Variant Property)を満たす方程式理論に焦点を当てている。 しかし、それらは手動で FVP を証明するか、少なくとも E-収束的書き換え系として表現するために必要であり、通常は E は結合的で可換な関数記号 (AC) の方程式理論である。 証明器 ProVerif は、表現を必要とせずに自動的に FVP を証明するため、これらのツールの中で唯一の例外である。 本研究では,FVPの特定表現を必要とせずにFVPを証明し,E-コンバージェント書き換えシステムによって表現される理論のクラスを超越した新たな半決定手順を提案する。 我々はプロトタイプを実装し、それを文献からいくつかの理論に適用することに成功しました。

関連論文リスト

• Equational Anti-Unification over Absorption Theories [1.124958340749622]
  抗統一技術は、クローン検出と自動プログラム修復法で使用されている。 本稿では、反統一変調純吸収理論、すなわち、いくつかの作用素は公理 $f(x,varepsilon_f) approx f(varepsilon_f,x) approx varepsilon_f$ を満たす特別な定数と関連している。 我々はこのような理論に対する健全で完全なルールベースのアルゴリズムを提供し、さらに、反統一モジュロ吸収は無限であることを示す。
  論文  参考訳（メタデータ） (2023-10-17T10:38:06Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  クロスモーダル検索手法は、共通表現空間を共同学習することにより、視覚と言語モダリティの類似性関係を構築する。 しかし、この予測は、低品質なデータ、例えば、腐敗した画像、速いペースの動画、詳細でないテキストによって引き起こされるアレタリック不確実性のために、しばしば信頼性が低い。 本稿では, 原型に基づくAleatoric Uncertainity Quantification (PAU) フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-09-29T09:41:19Z)
• Gaussian Process Probes (GPP) for Uncertainty-Aware Probing [61.91898698128994]
  モデルによって表現される概念に関する不確実性を探索し、測定するための統一的でシンプルなフレームワークを導入する。 実験の結果,(1)ごく少数の例でも,モデルの概念表現を探索し,(2)認識の不確実性(プローブがどの程度確実か)と解離不確実性(モデルがファジィか)を正確に測定し,(3)これらの不確実性尺度と古典的手法を用いて分布データの検出を行うことができた。
  論文  参考訳（メタデータ） (2023-05-29T17:00:16Z)
• All Roads Lead to Rome? Exploring the Invariance of Transformers' Representations [69.3461199976959]
  本稿では, ビジェクション仮説を学習するために, 非可逆ニューラルネットワーク BERT-INN に基づくモデルを提案する。 BERT-INNの利点は理論上も広範な実験を通じても明らかである。
  論文  参考訳（メタデータ） (2023-05-23T22:30:43Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  我々はCryptoVampire暗号プロトコル検証を初めて導入し、BC論理におけるトレース特性の証明を完全に自動化した。 主要な技術的貢献は、プロトコルプロパティの1次(FO)形式化と、サブターム関係の調整されたハンドリングである。 理論面では、全FO論理を暗号公理で制限し、HO BC論理の表現性を失うことにより、音質を損なわないことを保証する。
  論文  参考訳（メタデータ） (2023-05-20T11:26:51Z)
• An Analysis of Attention via the Lens of Exchangeability and Latent Variable Models [64.87562101662952]
  入力トークンは、位置エンコーディングを含むため、しばしば交換可能であることを示す。 我々は入力トークンの十分かつ最小限の表現の存在を確立する。 所望パラメータの注意が近似誤差まで潜伏した後部を推定することを証明する。
  論文  参考訳（メタデータ） (2022-12-30T17:59:01Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。 これは、説明に表される論理述語に基づいて、反実仮説を生成する。 そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
  論文  参考訳（メタデータ） (2022-05-25T03:40:59Z)
• Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
  自動定理証明(Automated Theorem Proving)は、いくつかの予想(クエリ)が一連の公理(事実と規則)の論理的な結果であることを示すことができるコンピュータプログラムの開発を扱う。 近年のアプローチでは、自然言語(英語)で表される公理の予想を導出するトランスフォーマーに基づくアーキテクチャが提案されている。 本研究は, 一般化の項における最先端結果を実現するニューラルユニファイザという, 新たなアーキテクチャを提案する。
  論文  参考訳（メタデータ） (2021-09-17T10:48:39Z)
• A Theory of Label Propagation for Subpopulation Shift [61.408438422417326]
  ラベル伝搬に基づくドメイン適応のための有効なフレームワークを提案する。 アルゴリズム全体でエンドツーエンドの有限サンプル保証を得る。 理論的なフレームワークを、第3のラベルなしデータセットに基づいたソースからターゲットへの転送のより一般的な設定に拡張します。
  論文  参考訳（メタデータ） (2021-02-22T17:27:47Z)

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

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