认证测试方法在安全协议形式化分析中的应用研究

《认证测试方法在安全协议形式化分析中的应用研究》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、上海交通大学硕士学位论文认证测试方法在安全协议形式化分析中的应用研究姓名：王鹏申请学位级别：硕士专业：通信与信息系统指导教师：陆松年20071201上海交通大学硕士学位论文认证测试方法在安全协议形式化分析中的应用研究摘要本文对认证测试方法在安全协议分析中的应用进行了深入研究，提出了扩展的认证测试方法并设计了基于该方法的协议分析算法和自动化协议分析系统。认证测试方法是一种基于串空间模型的安全协议验证方法，该方法的局限性在于忽视了测试的认证属性和加密密钥的关系。因此我们提出了密钥矩阵的概念，深入分析了在不同密钥加密的情况下的测试的属性,

2、证明了一系列用来分析和改进协议的定理，提出了扩展的认证测试方法。通过验证Needham-Schroeder协议、Yahalom协议和EAP-AKA协议，说明了扩展的认证测试方法具有证明过程简洁清晰，具有一定协议纠错能力的特点。基于扩展的认证测试方法，我们设计了自动化安全协议验证算法P算法。P算法可以同时对发起者和响应者进行验证，从而提高了协议验证效率。为了可以大规模分析协议，我们开发了形式化协议描述语言P语言及P语言语法解析器，极大的提高了系统的可用性。之后通过对Needham-Schroeder协议的验证说明了P算法运行的一般流程

3、。V上海交通大学硕士学位论文最后我们介绍了基于P算法的安全协议自动化分析系统，并使用该系统对Needham-Schroeder协议、NSL协议和Woo-Lam协议进行分析，分析结果与文献中相一致。关键词：安全协议，串空间模型，认证测试方法，扩展的认证测试方法，Ｐ算法VI上海交通大学硕士学位论文RESEARCHONTHEAPPLICATIONOFAUTHENTICATIONTESTSINFORMALANALYSISOFSECURITYPROTOCOLABSTRACTInthispaper,wedodeepresearchontheap

4、plicationofAuthenticationTestsinsecurityprotocolanalysis,andproposetheExpandedAuthenticationTests,basedonwhichwedesigntheautomaticsecurityprotocolanalysissystem.AuthenticationTestsisasecurityprotocolanalysismethodbasedonStrandSpace.ThedeficiencyofAuthentication

5、Testsisthatitoverlookstherelationshipbetweentestattributeandencryptedkey.ThereforeweintroducethedefinitionofKeymatrixandfocusontheattributeoftheauthenticationtestswithdifferenttypesofencryptedkeyandproposeaseriesofpropositionsforprotocolanalysisandrevision.Theseproposi

6、tionsVII上海交通大学硕士学位论文enhancetheoriginalauthenticationtestsmodel.TheanalysisandredesignoftheNeedham-Schroederprotocol，YahalomprotocolandEAP-AKAprotocolshowthattheExpandedAuthenticationTestsaremoreefficientcomparedwiththeinitialoneandhavetheabilitytorepairtheprotocolwithf

7、laws.BasedonExpandedAuthenticationTests,wedesigntheautomaticsecurityprotocolanalysisalgorithms:Palgorithms.Thisalgorithmcanprovebothinitiatorandresponderatthesametime,soitismoreefficient.Toanalyzelargeamountofprotocolsefficiently,wedesigntheformalprotocoldescriptionlan

8、guagePlanguage,anddeveloptheparserbasedonit.ByprovingNeedham-Schroederprotocol,weshowtheprocedureofPalgorithms.Atlast