Paper 2020/929 Original: eprint.iacr.org/2020/929 ↗
Local XOR Unification: Definitions, Algorithms and Application to Cryptography
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.
- History
- 2020-07-26: last updated
- 2020-07-26: published
- Short URL
- https://ia.cr/2020/929
- License
- https://creativecommons.org/licenses/by/4.0/
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}
}