Bounded ACh unification

DOI10.1017/S0960129520000183MaRDI QIDQ5139278zbMATH OpenFDO

Authors

Publication date 8 December 2020

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1811.05602

zbMATH Keywords

commutativitycryptographic protocol analysisequational unificationhomomorphismMauderewriting

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Cryptography (94A60)

Abstract: We consider the problem of the unification modulo an equational theory ACh, which consists of a function symbol $h$ that is homomorphic over an associative-commutative operator $+$. Since the unification modulo ACh theory is undecidable, we define a variant of the problem called extit{bounded ACh unification}. In this bounded version of ACh unification, we essentially bound the number of times $h$ can be applied to a term recursively, and only allow solutions that satisfy this bound. There is no bound on the number of occurrences of $h$ in a term, and the $+$ symbol can be applied an unlimited number of times. We give inference rules for solving the bounded version of the problem and prove that the rules are sound, complete, and terminating. We have implemented the algorithm in Maude and give experimental results. We argue that this algorithm is useful in cryptographic protocol analysis.

Recommendations

• Asymmetric unification: a new unification paradigm for cryptographic protocol analysis
• Unification Modulo Chaining
• scientific article; zbMATH DE number 4074540
• Efficient general AGH-unification
• Mechanizing Mathematical Reasoning

Cites work

• A decision algorithm for distributive unification
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Efficient general AGH-unification
• Efficient general unification for XOR with homomorphism
• scientific article; zbMATH DE number 3871322 (Why is no real title available?)
• scientific article; zbMATH DE number 2043528 (Why is no real title available?)
• Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties
• On unification modulo one-sided distributivity: algorithms, variants and asymmetry
• Term Rewriting and All That
• Unification modulo homomorphic encryption
• Unification modulo homomorphic encryption
• Unification problems with one-sided distributivity
• Unification theory

Cited in

(2)

• Unification modulo a 2-sorted equational theory for cipher-decipher block chaining
• Restricted unification in the DL \(\mathcal{FL}_0\)

Describes a project that uses

Uses Software

• Maude
• Maude-NPA

This page was built for publication: Bounded ACh unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5139278)