Formal Analysis And Verificaiton Of Ultralightweight RFID Mutual Authenticaiton Protocol With Model Checking

With a swift development,Internet of Things(IoT)has set off the third wave of world's information industry after which has been raised by Computer and Internet.Radio Frequency Identification(RFID)technique,as the critical technology of IoT,has been widely utilized in public service,intelligent transportation,smart home and other fields.However,RFID systems are more vulnerable to suffer malicious attacks,as the open wireless transmission channel is adopted within reader and tag.Ultralightweight mutual authentication protocol provides strong security for RFID systems,hence it is important to make sure that those protocols are secure.As a significant means of protocol security analysis,formal method can guarantee higher accuracy and reliability during the protocol analysis process.This paper concentrates on researching security issues of ultralightweight RFID mutual authentication protocol(UMAP).Two typical ultralightweight mutual authentication protocols,Type 1 scheme RCIA and Type 2 scheme RAPP,are selected as our study cases.Appying formal method to verify RCIA and RAPP respectly,our contributions are:(1)Protocol abstract modeling method is presented to overcome the limitation which is inconvenient to discuss security properties of UMAP directly with formal method.Hence,model checking technique can be applied to analyse RFID protocol.(2)Maggi modeling method is extended through implementing secret key selection and update operation in RFID protocol interaction.After RCIA and RAPP are modeled,we use SPIN to verify security properties of protocols,and results show that desynchronization attack exists in both RCIA and RAPP.(3)G-UMAP is built for characterizing session flow of Type 1 scheme and Type 2 scheme,and describing generalized desynchronization attack existed in G-UMAP.(4)A general patching scheme based on key synchronization mechanism is proposed for resisting desynchronization attack in G-UMAP.With using proposed patching scheme to improve the RCIA and RAPP protocol respectively,formal analysis indicates that improved RCIA and RAPP protocol both gains higher security.The protocol abstract modeling method has great significance in formal analysis for similar UMAPs;the proposed key synchronization mechanism is proved to be practical against desynchronization attack,and is applicable for design and analysis of similar UMAPs.