Automatic verification of Finite Variant Property beyond convergent equational theories

• URL: http://arxiv.org/abs/2410.15289v1
• Date: Sun, 20 Oct 2024 05:11:30 GMT
• Title: Automatic verification of Finite Variant Property beyond convergent equational theories
• Authors: Vincent Cheval, Caroline Fontaine,
• Abstract summary: Most automated verifiers for security protocols focus on equational theories that satisfy the Finite Variant Property (FVP) 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.
• Score: 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.

Related papers

• Equational Anti-Unification over Absorption Theories [1.124958340749622]
  Anti-unification techniques have found uses within clone detection and automatic program repair methods. This paper considers anti-unification modulo pure absorption theories, i.e., some operators are associated with a special constant satisfying the axiom $f(x,varepsilon_f) approx f(varepsilon_f,x) approx varepsilon_f$. We provide a sound and complete rule-based algorithm for such theories. Furthermore, we show that anti-unification modulo absorption is infinitary.
  arXiv  Detail & Related papers  (2023-10-17T10:38:06Z)
• Prototype-based Aleatoric Uncertainty Quantification for Cross-modal Retrieval [139.21955930418815]
  Cross-modal Retrieval methods build similarity relations between vision and language modalities by jointly learning a common representation space. However, the predictions are often unreliable due to the Aleatoric uncertainty, which is induced by low-quality data, e.g., corrupt images, fast-paced videos, and non-detailed texts. We propose a novel Prototype-based Aleatoric Uncertainty Quantification (PAU) framework to provide trustworthy predictions by quantifying the uncertainty arisen from the inherent data ambiguity.
  arXiv  Detail & Related papers  (2023-09-29T09:41:19Z)
• Gaussian Process Probes (GPP) for Uncertainty-Aware Probing [61.91898698128994]
  We introduce a unified and simple framework for probing and measuring uncertainty about concepts represented by models. Our experiments show it can (1) probe a model's representations of concepts even with a very small number of examples, (2) accurately measure both epistemic uncertainty (how confident the probe is) and aleatory uncertainty (how fuzzy the concepts are to the model), and (3) detect out of distribution data using those uncertainty measures as well as classic methods do.
  arXiv  Detail & Related papers  (2023-05-29T17:00:16Z)
• All Roads Lead to Rome? Exploring the Invariance of Transformers' Representations [69.3461199976959]
  We propose a model based on invertible neural networks, BERT-INN, to learn the Bijection Hypothesis. We show the advantage of BERT-INN both theoretically and through extensive experiments.
  arXiv  Detail & Related papers  (2023-05-23T22:30:43Z)
• CryptoVampire: Automated Reasoning for the Complete Symbolic Attacker Cryptographic Model [8.838422697156195]
  We introduce the CryptoVampire cryptographic protocol verifier, which for the first time fully automates proofs of trace properties in the BC Logic. Key technical contribution is a first-order (FO) formalization of protocol properties with tailored handling of subterm relations. On the theoretical side, we restrict full FO logic with cryptographic axioms to ensure that, by losing the expressivity of the HO BC Logic, we do not lose soundness.
  arXiv  Detail & Related papers  (2023-05-20T11:26:51Z)
• An Analysis of Attention via the Lens of Exchangeability and Latent Variable Models [64.87562101662952]
  We show that input tokens are often exchangeable since they already include positional encodings. We establish the existence of a sufficient and minimal representation of input tokens. We prove that attention with the desired parameter infers the latent posterior up to an approximation error.
  arXiv  Detail & Related papers  (2022-12-30T17:59:01Z)
• Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
  We introduce the methodology of Faithfulness-through-Counterfactuals. It generates a counterfactual hypothesis based on the logical predicates expressed in the explanation. It then evaluates if the model's prediction on the counterfactual is consistent with that expressed logic.
  arXiv  Detail & Related papers  (2022-05-25T03:40:59Z)
• Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
  Automated Theorem Proving deals with the development of computer programs being able to show that some conjectures (queries) are a logical consequence of a set of axioms (facts and rules) Recent approaches have proposed transformer-based architectures for deriving conjectures given axioms expressed in natural language (English) In this work we propose a new architecture, namely the Neural Unifier, which achieves state-of-the-art results in term of generalisation.
  arXiv  Detail & Related papers  (2021-09-17T10:48:39Z)
• A Theory of Label Propagation for Subpopulation Shift [61.408438422417326]
  We propose a provably effective framework for domain adaptation based on label propagation. We obtain end-to-end finite-sample guarantees on the entire algorithm. We extend our theoretical framework to a more general setting of source-to-target transfer based on a third unlabeled dataset.
  arXiv  Detail & Related papers  (2021-02-22T17:27:47Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.