Formal Analysis and Verification for Three-Party Authentication Protocol of RFID

RFID three-party authentication protocol based on NTRU cryptosystem is a type of multi-entities authentication protocol. Unlike other RFID mutual authentication protocols, this protocol realizes mutual authentication of Server to Reader, and Server to Tag. Model checking is a formal method to check the correctness specifications hold in each state on concurrent and distributed systems, which can be used to verify the security of network protocol. A multi-channels constructing method is proposed to build this protocol model for formal analysis, then authentication property of the protocol is verified by model checker SPIN. Formal verification result reveals that an attack exists in this protocol, hence the protocol cannot guarantee the security of the three-party authentication protocol. The modeling method proposed above has great significance on security analysis for such three-party authentication protocols.