Classification, formalization and automatic verification of untraceability in RFID protocols

Radio Frequency IDentification (RFID) is the wireless non-contact use of radio-frequency electromagnetic fields to transfer data, for the purposes of automatically identifying and tracking tags attached to objects. Since RFID tags can be attached to clothing, possessions, or even implanted within people, the possibility of reading personally-linked information without consent has raised privacy concerns. Privacy is the essential part of today's society.;RFID protocols are subsets of cryptographic protocols but with lightweight cryptographic functions. Their main objective is identification with respect to some privacy properties, like untraceability. An RFID identification protocol should not only allow a legitimate reader to authenticate a tag but also it should protect the privacy of the tag. Although design and implementation of cryptographic protocols are tedious and time consuming, security flaws have been discovered in most of these protocols. Therefore the responsibility for reliable and proper verification becomes crucial.;Formal methods can play an essential role in the development of reliable security protocols. Critical systems which requires high reliability such as security protocols are difficult to be evaluated using conventional tests and simulation techniques. This has encouraged the researchers to focus on the formal verification techniques to ensure a high degree of reliability in such systems. In spite of the studies which have been carried out in this field, an explicit definition for some of these security properties is still missing.;The main goal of this work is to demonstrate the use of formal methods to analyse RFID protocol's untraceability. Untraceability generally defined as ensuring that an attacker can not get any information to be used to trace an object in time and space. Several definitions are discussed in the literature for untraceability property, however, there is no compromise on its exact definition. We have introduced three different levels for this property. We also have classified all former definitions of untraceability property in the literature. In order to create a model for a protocol and define privacy properties, our approach employs process calculi technique, applied pi calculus. We have demonstrated the formal definitions of suggested untraceability levels, extending them to some case studies on the existing protocols.;Keywords: RFID security protocol, privacy, untraceability, formal method, process algebra, applied pi.