基于串空间模型的安全协议形式化验证方法的研究

《基于串空间模型的安全协议形式化验证方法的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、≥谤爻龟走海博士学位论文DoCToRA工DISSERTAT【oN论文题目基于串空间模型的安全协议形式化验证方法的研究学科专业望堕量堡墨堡丝——作者姓名至盟垩指导教师』世主L垒整生—垫塑答辩日期!!!!±!!上海交通大学博士学位论文然蜃，叛改遂翳认证测试方法热麓萋窭，提出了安全垮议麴认涯属牲中不仪要满足一致髋璃性，还要满足测试分基的唯一性属髓。通过定义测试分量唯一性，排除由于消息重放而引起攻击的可能性。并提出了安全协议自动化验证算法——AAAP(AutomaticAnalyzerofAuthenticationProtocols)，AAAP霉法在多季孛认涯协议证明中的应用说明了该

2、算法能够有效发现协议中存在的漏洞著及时终止算法的运行；而与类似算法相比，AAAP算法在协议验证中具有遍历状态空问少、运牙效率薅夔饶点。最后，基于AAAP算法开发了安全协议自动化验证原型系统，并通过对多个经典认证协议的实验验证说明该原型系统的有效性。本文镧藏性魏工撵主要有：1．改进了认证测试方法，使之能够为对称密铜协议提供更为完善的验证。通过引入消息类型的概念，提出了基于消息类裂检测的改进认证测试方法，矮予稔凝耱莰孛爨否存在鑫漕惑重放悉弓l麓黥攻击，勰次了藏骞试溪溅试方法无法发现重放攻击的问题，在理论上具有创新性。2．提出了测试分量唯一性属性，完善了协议认诞属性的描述。通过对测试

3、分量壤一缝豹迂爨，验证换议摄挠重效玫壹黟瓷壅玫麦夔熊力，在理论，皇爨有创新性。3．提出了基于改进认证测试方法的AAAP算法。通过对协议～致性属性和唯一楚瓣经翡蠡动纯涯羁，验逐协议能够这蘩瓣安全毽菰。AAAP算法鼹多种认诚协议的验证说明该算法能够及时发观协议中存在的漏洞并终止协议运行，与同类型算法相比资源耗费小，在理论的应用上具有创新的特虑。4．开发了基于AAAP箨法豹安全秘议謇动稼验涯琢壅系统，将理论穰羹艨黉于实际的安全协议验证。应用该原型系统验证了Nee曲am．Schroeder公钥协议、NSL协议、Neuman-Stubblebine认证协议、Woo—Lain单向认证协议的

4、安全悔，验话豹络莱与使焉瑶论模鼙匏验谖绦莱买育较强弱一致洼，在遴论的应用上具有创新的特点。关键词安全协谈，率空阍模型，试诞漠l试方法，敬迸的试谣测试方法，AAAP算法，认ui芷协议llt海交通大学博士学位论文RESEARCHoNFoRMALVERIFICATIoNMETHoDSOFSECURITYPRoToCoLSBASEDoNSTRANDSPACEMoDELABSTRCTSecurityprotocolsworks∞akindofthekerneltechnologyforthesecurenetworkcommunication，thustheircoIrectncssar

5、eVerycrucialtonetworksecurity．However,thesecurityprotocoldesignisallerror-proneprocess．Theproblems．whicharehowtoanalyzethesecurityprotocolstoensuretheirsafetyandvalidity,howtodeignthesecurityprotocolstoensuretheircorrectness，andhowtoimprovetheemcieIlcyoftheautomaticverificationtools，shouldbe

6、solvedbyformalmethodsforsecurityprotocols．Untilnow,manykindsofformalmethodshavebeenpresentedforsecurityprotocolanalysisanddesign．Althoughtheformalmethodshavebeensucceededinfindingflawsandattacksofmanysecurityprotocols，theystillsufferfromlotsofproblems，suchasthefaultinessoftheformalmethoditse

7、lf,lackofautomatictoolsupportbecauseofthecomplextheoreticmodel，andresource-exhaustingproblemincurrentamomaticverificationtools．Whereas，inthisthesis，wemakefurtherresearch011theaboveareasbasedon-thes嘶dspacemodelandauthenticationtests．proposesomeeffic