基于spi演算的安全协议形式化分析

《基于spi演算的安全协议形式化分析》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、ADissertationSubmittedtoShanghaiJiaoTongUniversityfortheDegreeofMasterofScienceFORMALANALYSISOFSECURITYPROTOCOLSBASEDONSPICALCULUSAuthor：QingxiongZhengSpecialty:ComputerScienceAdvisor:Prof.YuxiFuSchoolofElectronicsandElectricEngineeringShanghaiJiaoTon

2、gUniversityShanghai,P.R.ChinaMarch,2010基于Spi演算的安全协议形式化分析摘要安全的密码协议是构筑信息安全体系的基础，是网络通信和应用必不可少的组件之一。不过，已有的安全协议往往被证实并不如它们的设计所期望的那样安全。由于安全协议具有安全目标定义的微妙性，运行环境的复杂性，攻击者能力的不确定性和协议执行的高并发性，验证安全协议具有很多难点。因此我们必须借助形式化的方法对安全协议进行安全分析和验证。自上个世纪七十年代末以来，人们提出了多种安全协议分析的形式化理论，

3、主要有基于知识与信念推理的模态逻辑方法，基于定理证明的方法和基于进程演算的方法三种。其中，基于进程演算的方法对于协议的描述十分接近协议的本身含义，可以很精确地刻画协议的整个交互过程。Spi演算是在经典进程演算理论的基础上，为刻画安全协议而专门提出来的一种演算。Spi演算扩展了基本的密码操作原语，适合多轮并发条件下安全协议的分析验证。本文对基于进程演算的验证方法作了一定的研究，以Spi演算为核心，依托互模拟等价技术对安全协议进行分析。论文主要内容包括：1）总结安全协议验证的几种形式化方法，论述其主要概

4、念以及验证实现的基本思想，深入探讨基于进程演算的协议分析方法。并以Spi演算为基础，以互模拟等价关系理论为依托，对协议验证分析的整个过程进行梳理。2）对如何利用pi演算对安全协议进行初步描述进行了表述，在这个过程中，讨论了引入Spi演算的必要性。对强互模拟等价关系的语义进第I页行阐述和分析，并指出其在协议验证中过于严格，进一步，引入测试等价刻画协议的安全属性。3）为了简化协议的验证过程，本文介绍了框架互模拟关系和barbed同余关系在验证过程中的作用，描述它们和测试等价之间的联系。并且讨论了Spi演

5、算在非对称密码体系下的语法语义。最后，利用Spi演算对经典协议进行了验证分析。关键词：安全协议，形式化方法，进程演算，Spi演算，互模拟第II页FORMALANALYSISOFSECURITYPROTOCOLSBASEDONSPICALCULUSABSTRACTAsafecryptographicprotocolisthebasisofcomposinginformationsecuritysystems,anditisoneofabsolutelynecessarycomponentsofthec

6、ommunicationofnetworksanditsapplications.However,manyexistingsecurityprotocolsareprovennottobesoreliableaswhatwereexpected.Owingtothesubtletyofsecuritygoal,thecomplexityofnetworkenvironment,theuncertaintyofthepenetrator'sabilityandthehighparallelizatio

7、nofprotocolrun,verificationofasecurityprotocolcanbeverydifficult,sowemustanalyzesecurityprotocolsbyformalmethods.Sincethe1970's,someformalmethodsofsecurityprotocolanalysishavebeenproposed,thesemethodsaremainlyofthreekinds:methodsbasedonmodallogicofknow

8、ledgeandbelief,methodsbasedontheoremproofandmethodsbasedonprocesscalculus.Andamongthethreemethodsmentionedabove,theprocesscalculuscanmodeltheprotocolsveryprecisely.TheSpicalculus,whichisbasedonthetheoryofprocesscalculus,candefinecryptog