基于模型检测的超轻量级RFID双向认证协议形式化分析与验证

《基于模型检测的超轻量级RFID双向认证协议形式化分析与验证》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号______________________________密级______________________________ＵＤＣ______________________________编号______________________________硕士学位论文基于模型检测的超轻量级RFID双向认证协议形式化分析与验证学位申请人：李伟学科专业：计算机软件与理论指导教师：肖美华教授答辩日期：独创性声明本人郑重声明：所呈交的学位论文是我个人在导师指导下进行的研究工作及取得的研究成果。尽我所知，除了文中特别加以标

2、注和致谢的地方外，论文中不包含其他人已经发表和撰写的研究成果，也不包含为获得华东交通大学或其他教育机构的学位或证书所使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示了谢意。本人签名_______________日期____________关于论文使用授权的说明本人完全了解华东交通大学有关保留、使用学位论文的规定，即：学校有权保留送交论文的复印件，允许论文被查阅和借阅。学校可以公布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论文。保密的论文在解密后遵守此规定，无保密内

3、容。本人签名____________导师签名__________日期___________摘要基于模型检测的超轻量级RFID双向认证协议形式化分析与验证摘要物联网的飞速发展掀起了继计算机、互联网后世界信息产业的第三次浪潮。RFID技术作为物联网的核心技术，被广泛运用于公共安全、环境监测、智能交通、智能家居等领域。然而，RFID中阅读器与标签之间的无线通信方式使RFID系统更易遭受安全攻击。RFID安全认证协议是保障RFID系统通信安全的有效途径，协议自身安全性至关重要。形式化方法作为协议安全性分析的重要手段，可保证协

4、议分析过程的准确性和可靠性。本文重点关注超轻量级RFID双向认证协议的安全性问题。选取两个典型的超轻量级双向认证协议，Type1型协议RCIA和Type2型协议RAPP作为研究对象，采用形式化方法分别分析RCIA和RAPP协议的安全性，所取得研究成果有：（1）提出协议抽象建模方法。克服因超轻量级RFID双向认证协议底层加密复杂，而不便于直接使用形式化方法分析的局限，使模型检测技术能应用于RFID协议分析领域。（2）拓展Maggi的Promela建模方法。实现超轻量级安全认证协议交互过程中特有的密钥选择和密钥更新操作，

5、运用SPIN工具验证得到RCIA和RAPP中均存在去同步攻击漏洞。（3）构建超轻量级双向认证协议通用模型G-UMAP。统一描述Type1和Type2型协议交互流程，以及G-UMAP中的去同步攻击漏洞。（4）提出基于G-UMAP密钥同步机制的漏洞通用修补方案，分别对RCIA和RAPP协议进行改进。改进协议形式化验证结果表明，改进后的RCIA和RAPP协议具有更高安全性。本文提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义；提出的基于密钥同步机制的漏洞通用修补方案，被证明能有效抵御去同步

6、漏洞，可适用于此类超轻量级RFID双向认证协议的设计和分析。关键词：RFID双向认证协议，RCIA，RAPP，形式化方法，模型检测，协议抽象建模IAbstractFORMALANALYSISANDVERIFICAITONOFULTRALIGHTWEIGHTRFIDMUTUALAUTHENTICAITONPROTOCOLWITHMODELCHECKINGABSTRACTWithaswiftdevelopment,InternetofThings(IoT)hassetoffthethirdwaveofworld'sinf

7、ormationindustryafterwhichhasbeenraisedbyComputerandInternet.RadioFrequencyIdentification(RFID)technique,asthecriticaltechnologyofIoT,hasbeenwidelyutilizedinpublicservice,intelligenttransportation,smarthomeandotherfields.However,RFIDsystemsaremorevulnerabletosu

8、ffermaliciousattacks,astheopenwirelesstransmissionchannelisadoptedwithinreaderandtag.UltralightweightmutualauthenticationprotocolprovidesstrongsecurityforRFIDsystems,henceit