Formal Analysis of OTag Protocol on Authentication and Confidentiality

A novel RFID Tag architecture called OTag (Object Tag) and its protocol was designed to enhance the communication among real world objects. ITS (Intelligent Transportation System) was selected as the very first candidate to adopt above technology. Three actors of ITS; vehicle, user and infrastructure were represented as relevant instances of OTag class to enable the communications. To assure the security and privacy of above communications, five sub protocols: non encrypted reading, encrypted reading, encrypted writing, ownership transferring, and key updating were evaluated using formal analysis technique. First of all, the five protocols were modeled in formal language called HLPSL. Then the validation of the modeled protocol representations was conducted by using a tool called SPAN. After that, those five protocols were executed against the modeled intruder to verify desired security goals to verify the strengths and weakness by using AVISPA. Finally, results of each execution were analyzed to derive the concluding remarks.