You are looking at a specific version 20200726:063025 of this paper.
See the latest version.
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)
- Category
- Foundations
- Publication info
- Preprint.
- Keywords
- foundationsformal 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