2008/08/05 by Ralf Kuesters, R. Kuesters, Kuesters, Ralf +2
Computer Science · #Advanced Authentication Protocols Security #Cryptography and Security (cs.CR) #Digital Rights Management and Security #FOS: Computer and information sciences #User Authentication and Security Systems #cs.CR
paper · pdf · doi:10.48550/arxiv.0808.0634
arxiv created 2008/08/05 · openalex publication_date 2008/08/05 · arxiv updated 2009/12/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/01
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.