Cryptology ePrint Archive: Report 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.

Category / Keywords: foundations / foundations, formal methods

Date: received 25 Jul 2020, last revised 25 Jul 2020

Contact author: hlin at clarkson edu,clynch@clarkson edu

Available format(s): PDF | BibTeX Citation

Version: 20200726:063025 (All versions of this report)

Short URL: ia.cr/2020/929


[ Cryptology ePrint archive ]