安全协议的概率模型检测

《安全协议的概率模型检测》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、密级：中国科学院大学UniversityofChineseAcademyofSciences一硕士学位论文2013年5月TingWangAThesisSubmittedtoTheUniversityofChineseAcademyofSciencesInpartialfulfillmentoftherequirementForthedegreeofMasterofEngineeringInstituteofInformationEngineeringMay,2013中国科学院信息工程研究所研究生学位论文独创性声明本人声明所呈交的学位论文是本人在姬东耀导师指导下进行的研究工作

2、及取得的研究成果。除了文中特别加以标注和致谢的内容外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得中国科学院信息工程研究所或其他教育机构的学位或证书而使用过的材料。与我共同工作的同志对本研究所做的任何贡献均己在论文中做了明确的说明并表示谢意。论文与资料若有不实之处，本人承担一切相关责任。学位论文作者签名：签字日期：M≥年S月11日学位论文版权使用授权说明本学位论文作者完全了解中国科学院信息工程研究所有关保留、使用学位论文的规定。特授权中国科学院信息工程研究所可以将学位论文的全部或部分内容编入有关数据库进行检索，并采用影印、缩印或扫描等复制手段保存、汇编，以供

3、查阅和借阅。同意研究所向国家有关部门或机构送交论文的复印件和磁盘。(保密的论文在解密后应遵循此规定)学位论文作者签名：王培签字日期：如I31年S月几日聊虢姆t童径柳砌瞻厂月『7日摘要系统的安全性得到越来越多的重视和研究，在软件或硬件设计之初如果能验证系统的安全性，就可以减少很多损失。模型检测是一种形式化验证技术，主要用来验证系统是否满足它所要求的一些性质。但是经典的模型检测验证的都是定性的性质，缺乏对系统量化性质的分析。概率模型检测弥补了这种不足，概率模型检测主要分析系统的量化性质。本文首先介绍了概率模型检测的研究现状，随后介绍了经典的模型检测方法，并总结了我们之前的部分工

4、作一应用模型检测工具Alloy来找出组播密钥管理协议中存在的漏洞。然后介绍了概率模型检测、概率计算树逻辑(PCTL)和概率模型检测器PRISM。同时，本文还介绍了DoS攻击及利用puzzle来避免DoS攻击，随后介绍了两种主机标识协议(HostIdentityProto-col，HIP)，并对其中一个协议进行了纠错及修改，分析其中依旧存在DoS攻击。最后着重介绍了我们如何利用PRISM来分析DoS攻击对主机标识协议HIP的威胁。关键词：模型检测，概率模型检测，HIP协议，PRISMAbstractThesecurityofsystemshasgotmoreandmorere

5、searchandemphasis，sincealotoflosscanbeavoidedifdesignerscouldverifythesecurityofsystems，suchashardwareandsoftware，whiledesigningthem．Fortunately,ModelCheckingcailhelpdesignerstoverifysecurityofsystems．AsakindofFormalMethods，ModelCheckingismostlyusedtocheckwhetherthesystemmeetstherequiredpr

6、operties，whichistheclassicalmodelchecking．Thoughtheclassicalmod-elcheckinghasmanyadvantages，itonlychecksthequalitativepropertiesandcannotanalyzethequantitativeproperties．ThisshortageisremediedbyProb-abilisticModelCheckingwhichcananalyzeboththequalitativepropertiesandthequantitativeproperti

7、es．Inthisthesis，wefirstlyintroducetheresearchaboutProbabilisticModelChecking，thenpresentthedetailsoftheclassicalmodelcheckingandProba-bilisticModelChecking，andsummarizepartofmypreviouslyworkabouttheclassicalmodelchecking，i．c．usingmodelcheckerAlloytoanalyzethem