Improving Automatic Verification Of Security Protocols With XOR

Cryptographic security protocols typically consist of a series of message exchanges among two or more agents over a hostile network. They aim to achieve various security goals such as authentication, secrecy, key agreement, privacy, and anonymity. However, designing secure protocols is an error-prone task and incorrect protocols may become ideal entry points for various attacks. Starting from the seminal work by Lowe [1], automated symbolic verification methods for security protocols have shown their strength in finding attacks and proving correctness of security protocols.As attacks that rely on cryptographic primitives are hard to prove and difficult to be automatically checked, cryptographic primitives are usually treated as functions without any algebraic properties in symbolic methods. This is called the perfect cryptography assumption [2], namely no cryptographic message can be opened without the correct key. Based on this assumption, many automatic tools have been designed and implemented, among which ProVerif [3] is considered as the state of the art [4]. However, ProVerif cannot uncover attacks that make use of certain algebraic properties of cryptographic primitives. Therefore, some relaxation of the perfect assumption needs to be investigated.Exclusive or (XOR) is one binary operator with typical algebraic properties that has drawn a lot of interest. For example, XOR is often used in radio frequency identification (RFID) systems, which have become popular in recent years. In order to detect attacks on XOR-protocols, we need to model intruders with the ability of exploring the above algebraic properties, in addition to the perfect cryptography assumption.Kusters and Truderung recently proposed an automatic verification method for security protocols with exclusive or ((?)). Their method reduces protocols with (?) to their (?)-free equivalents, enabling efficient verification by tools such as ProVerif. Although the proposed method works efficiently for verifying secrecy, verification of authentication properties is inefficient and sometimes impossible.In this thesis, we improve the work by Kusters and Truderung in two ways. First, we extend their method for authentication verification to a richer class of XOR-protocols by automatically introducing bounded verification. Second, we improve the efficiency of their approach by developing a number of dedicated optimizations. We show the applicability of our work by implementing a prototype and applying it to both existing benchmarks and RFID protocols. The experiments show promising results and uncover a flaw in a recently proposed RFID protocol.