Local XOR Unification: Definitions, Algorithms and Application to Cryptography

Hai Lin; Christopher Lynch

Paper 2020/929

Local XOR Unification: Definitions, Algorithms and Application to Cryptography

Hai Lin and Christopher Lynch

Abstract

Unification techniques have been proven to be useful for formal analysis of cryptographic systems. In this paper, we introduce a new unification problem called local XOR unification, motivated by formal analysis of security of modes of operation. The goal in local XOR unification is to find a substitution making two terms equivalent modulo the theory of exclusive-or, but each variable is only allowed to be mapped to a term from a given set of terms. We present two versions of the local XOR unification problem, and give algorithms to solve them, proving soundness, completeness and termination.

Metadata

Available format(s): PDF
Category: Foundations
Publication info: Preprint.
Keywords: foundations formal methods
Contact author(s): hlin @ clarkson edu
clynch @ clarkson edu
History: 2020-07-26: received
Short URL: https://ia.cr/2020/929
License: CC BY

BibTeX

@misc{cryptoeprint:2020/929,
      author = {Hai Lin and Christopher Lynch},
      title = {Local {XOR} Unification: Definitions, Algorithms and Application to Cryptography},
      howpublished = {Cryptology {ePrint} Archive, Paper 2020/929},
      year = {2020},
      url = {https://eprint.iacr.org/2020/929}
}