Formal Analysis and Verification for an Ultralightweight Authentication Protocol RAPP of RFID

Radio Frequency Identification (RFID) technique, as the core of Internet of Things, is facing security threats. It is critical to protect information security in RFID system. Ultralightweigh authentication protocols are an important class of RFID lightweight authentication protocols. RAPP is a recently proposed ultralightweight authentication protocol, which is different from any other existing protocols due to the use of permutation. Formal methods are vital for ensuring the security and reliability of software systems, especially safety-critical systems. A protocol abstract modeling method is presented to build abstract interaction model of RAPP which can be formalized by extracting interaction features. Due to the complexity of fundamental cryptograph operations in RAPP, the proposed method overcomes the limitation which is inconvenient to discuss security of RAPP directly with formal method. Using SPIN, authenticity and consistency of RAPP properties is verified. Analysis and verification result shows that RAPP is vulnerable against desynchronization attack. The proposed modeling method above has great significance in formal analysis of similar ultralightweight authentication protocols of RFID.