Security of RFID protocols

Radio-frequency identification (RFID) is a technology that uses radio waves to exchange data between RFID readers and tags. The low manufacturing costs and small size and the lack of need of a power source make RFID tags useful in many applications, but also impose a strong need for secure RFID protocols. The first part of this thesis considers the analysis of untraceability of RFID protocols. We start by designing a formal syntax and semantics for security protocols. We define untraceability as a property on the traces of a protocol. We find new untraceability flaws in a number of RFID protocols. Furthermore, we show that indistinguishability-based proof models are incomparable to unpredictability-based proof models. The second part of this thesis is concerned with authentication of RFID protocols. Authentication ensures that agents can not be impersonated. We categorize new authentication attacks into algebraic replay attacks, man-in-the-middle attacks, compositionality attacks, and cryptanalytic attacks. The third part of this thesis deals with formalizing ownership in RFID systems and related security properties. In dynamic environments where RFID tags are exchanged, sold, or traded, the owner of a tag may change. We define secure ownership, exclusive ownership, secure ownership transfer, and desynchronization resistance. The fourth part of this thesis describes the problem of recovering memory structures of systems. We define the carving problem as recovering the structure of the memory, based on an attributed dump set. We design and implement algorithms to find commonalities and dissimilarities and apply them to a deployed RFID system.