Radio Frequency Identification (RFID) is automatic object identifying technology which is one of the promising technologies in ubiquitous computing area. It allows us to identify number of products without any physical and visual contact. Recently, RF...
Radio Frequency Identification (RFID) is automatic object identifying technology which is one of the promising technologies in ubiquitous computing area. It allows us to identify number of products without any physical and visual contact. Recently, RFID was spotlighted by lots of its merits such as convenience and pervasiveness. Many attempts to adapt RFID system into many areas are in progress world-widely.
However, due to the wireless communication channel between readers and tags, serious privacy problems such as the data leakage and data traceability can be occurred. Therefore, many kinds of security protocols have been proposed to resolve these vulnerabilities. However the most of their protocol design were not verified with precise and logical methods, so the security robustness against the adversarial attacks cannot be guaranteed. Hence, we cannot assure that the previous work is worth to implement for the RFID system security protection.
In this thesis, firstly, we described two major security properties, the secrecy and authenticity, for the RFID system. Then we verify the previous work focus on these two properties by using precise and logical verification methods which is formal method. The result of the formal verification showed that the secrecy and authenticity were not satisfied in previous work. Finally, we designed a new security protocol which satisfies those two security properties using one-time pad. Our protocol is also formally verified its security robustness as we did on the previous work. The result of our protocol verification was positive.