安全协议进化生成与模态逻辑验证研究

《安全协议进化生成与模态逻辑验证研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、中国科学技术大学博士学位论文安全协议进化生成与模态逻辑验证研究姓名：毛晨晓申请学位级别：博士专业：计算机应用指导教师：王煦法20050501摘要中国科学技术人学博士学位论文性、认证性、不叮否认性、保密性、原子性、以及交易规模和协议效率方面等性质的电子商务协}义。(4)深入地研究了基于模态逻辑的安全协议形式化验证方法。①提出了用模态逻辑来分析安全协议密码系统相关缺陷的方法。其基本思想是扩展Dolev．Yao密码系统模型，不采用完善的密码系统假设。具体而言，本论文以CKT5逻辑为基础，以对称密码算法为重点，将序列密码和分组密码算法的特性以逻辑推理规则的形式引入到CKT5逻辑框架中，使得扩展后的

2、CKT5逻辑能够用于分析安全协议密码系统相关缺陷。②提出了用模态逻辑来分析安全协议猜测攻击的方法。其基本思想是增强Dolev-Yao攻击者模型，使攻击者具备密码分析能力。具体而言，以CKT5逻辑为基础，进行了多方面的扩展。首先增加了公钥密码体制和Vemam加密机制，增强了其描述协议的能力。接着在CKT5逻辑中引入了一组规则使主体具备猜测和验证口令的能力。然后给出在线猜测攻击定理以反映在线猜测攻击的特点。并通过相关定理的证明，简化了猜测攻击的分析过程。扩展后的CKT5逻辑能够用于分析安全协议的多种猜测攻击，且比现有方法更加简洁和商效。安全协议自动生成与验证研究是安全协议研究领域的热点和难点之

3、一。安全协议自动生成与验证研究，能够促进安全协议设计的自动化，以满足不断增长的安全协议应用需求。安全协议的自动生成与验证，不但具有重要的研究价值，而且对于解决安全协议难于设计的问题有着引人注目的现实意义和广阔的应用前景。ll关键词：安全协议：进化计算：形式化验证；模态逻辑Abstract中国科学技术大学博士学位论文AbstractWithcomputernetworksbecomingmoreandmorepopularizedinsocialproductionanddailylife，andalsowiththerapiddevelopmentofnetworkeconomyofwhi

4、che-commerceisatypicalrepresentation，securityprotocolsplaymoreandmoreimportantrolesinthefieldsofIntemet—basedpersonalandcommercialtransactions．Inthesefieldsthereisafastincreasingdemandforsecufityprotocols．However,itisnotoriouslydifficulttodesignandanalyzesecurityprotocols，Thepurposeofthisdissertat

5、ionistoexploreandresearchintoformalandautomatedarialysisanddesignmethodsofsecufityprotocols，Automaticgenerationandverificationofsecurityprotocolsisstudiedfromseveralaspectsincludingmodels，methodsandapplications．Amodelforautomaticgenerationandverificationofsecurityprotocolsisgivenatfirst．Thenametho

6、dforautomaticgenerationandverificationofauthenticationprotocolsispresentedtovalidatethemodel．Thereafter,foltherresearchesintotwokeypointsofthemodeIarecarriedout，includinggenerationapproachesandverificationapproaches．Themainresearchworkofthisdissertationcanbesummarizedasfollows：(1)Amodelforautomati

7、cgenerationandverificationofsecurityprotocolsisgiven，whichisusedtoguidetheresearchofautomaticgenerationandverificationmethodsofsecurityprotocolsTwokeypointsofthemodelarepointedout，i．e．generationapproachesandverif