Automatic verification of Finite Variant Property beyond convergent equational theories
Fuente:
arXiv
Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909356846481408 |
|---|---|
| author | Cheval, Vincent Fontaine, Caroline |
| author_facet | Cheval, Vincent Fontaine, Caroline |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_15289 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Automatic verification of Finite Variant Property beyond convergent equational theories Cheval, Vincent Fontaine, Caroline Cryptography and Security C.2.2; D.2.4; F.3.1 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. |
| title | Automatic verification of Finite Variant Property beyond convergent equational theories |
| topic | Cryptography and Security C.2.2; D.2.4; F.3.1 |
| url | https://arxiv.org/abs/2410.15289 |