Security Protocols for Low Cost RFID Tags: Analysis and Automated
Verification of Proposed Solutions
Esteban Masobro Garcia
RFID technology offers a number of advantages that make it stand out
amongst available auto- ID technologies. It has already been applied
in many areas, from large retail stores to car immobilisers and even
human beings. Nevertheless, the upcoming widespread adoption of RFID
requires the incorporation of suitable privacy and security
measures. Security protocol proposals constitute a major mechanism to achieve that goal. However, it must be emphasised that security
protocol design is an error-prone task. Consequently, it is essential to have automated tools at our disposal that can formally verify, to some extent, those protocols. The importance of a proof of security is vital in a field where security and privacy are under the spotlight. This project sets out to work on and contribute knowledge to this subject area.
In order to pursue the aforementioned aim, this project features
several objectives, the description of which accurately delineates the work that has been done. In the first place, a literature review is carried out on RFID security and privacy, with a focus on protocol proposals. At the same time, a number of security properties which have been found to cover adequately the security and privacy requirements of the field are identified. This is followed by three very detailed case studies, in the form of security protocols, along with suggestions for their improvement. At this point, the project turns to the classification of fifteen security protocols. The resulting comparison is critically analysed. Finally, four tools for the automated formal verification of security protocols are examined, leading to several proposals for the improvement of these tools to better meet the requirements of security protocols for low-cost RFID tags.
The contribution of this project has been three-fold. Firstly, an
improved version has been presented for each of the three protocols
examined as case studies: namely the Henrici and Muller protocol [11], the Alomair et al protocol [12], and the C2 scheme [13]. Secondly, as already mentioned, a classification of fifteen security protocols is presented and critically analysed. Finally, as also noted, there are a number of suggestions for the improvement of the tools for the automated formal verification of security protocols. These improvements have to do with the ability of the tools to better capture the requirements of security protocols for low-cost RFID tags.