Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach

TL;DR

This paper presents a method to reduce the analysis of cryptographic protocols involving XOR to an XOR-free case, enabling the use of existing tools like ProVerif for protocols previously hard to analyze.

Contribution

It introduces a reduction technique for Horn theories with XOR to XOR-free theories, broadening the applicability of existing protocol analysis tools.

Findings

Successfully reduced XOR-based protocol analysis to XOR-free case

Implemented the reduction and integrated with ProVerif

Discovered a new attack on a protocol using XOR

Abstract

In the Horn theory based approach for cryptographic protocol analysis, cryptographic protocols and (Dolev-Yao) intruders are modeled by Horn theories and security analysis boils down to solving the derivation problem for Horn theories. This approach and the tools based on this approach, including ProVerif, have been very successful in the automatic analysis of cryptographic protocols w.r.t. an unbounded number of sessions. However, dealing with the algebraic properties of operators such as the exclusive OR (XOR) has been problematic. In particular, ProVerif cannot deal with XOR. In this paper, we show how to reduce the derivation problem for Horn theories with XOR to the XOR-free case. Our reduction works for an expressive class of Horn theories. A large class of intruder capabilities and protocols that employ the XOR operator can be modeled by these theories. Our reduction allows us to carry out protocol analysis by tools, such as ProVerif, that cannot deal with XOR, but are very efficient in the XOR-free case. We implemented our reduction and, in combination with ProVerif, applied it in the automatic analysis of several protocols that use the XOR operator. In one case, we found a new attack.