基于进程演算的安全协议形式化研究.pdf

《基于进程演算的安全协议形式化研究.pdf》由会员上传分享，免费在线阅读，更多相关内容在应用文档-天天文库。

1、基于进程演算的安全协议形式化研究FormalResearchofSecurityProtocolsBasedOnProcessCalculus研究生：李国强导师：傅育熙教授专业：计算机软件与理论完成日期：2005年1月基于进程演算的安全协议形式化研究摘要随着网络技术应用与发展逐步渗透到许多关键部门，各种安全需求日渐复杂。然而，已有的安全协议往往被证实并不如它们的设计所期望的那样安全。同时，网络系统仍然面临着各种新、旧攻击手段的威胁。这种复杂的网络环境使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击，从而达到破坏网络安全的目的，因此，安全协议已成为网络安全的关键。安

2、全协议形式化分析技术可使协议设计者通过系统分析将注意力集中于接口、系统环境的假设、在不同条件下系统的状态、条件不满足时出现的情况以及系统不变的属性，并通过系统验证，提供协议必要的安全保证。目前，国内外形式化研究安全协议主要有基于知识与信念推理的模态逻辑方法，基于定理证明的方法和基于进程演算的方法三种。其中，进程演算对于协议的描述几乎接近协议的本身含义，可以很精确地刻划协议的运行过程。使用进程演算对安全协议分析和验证时，协议的每一个主体都被建模为一个单独的进程，这些子进程并发运行，并使用进程之间的共享通道进行同步通信，这样得到的并发系统将作为安全协议的基本模型。利用进程演

3、算对安全协议进行分析和验证时，既借鉴了进程演算作为代数模型的基本验证理论与方法，又使用了进程演算作为抽象程序设计语言的程序分析方法。因此，基于进程演算的安全协议验证技术可分为模型检测技术、互模拟验证技术和程序分析技术三种。本文在基于进程演算方法方面作了一定的研究，并且对本方向的研究2摘要前景作了总结和展望。论文主要内容及创新点包括：(1)在对Spi演算的研究中，定义了一个原语，解决了原演算不能验证存在时间戳的安全协议的各种验证，并基于扩展了的Spi演算，验证了Kerberos协议的认证性。(2)目前，安全协议形式化研究尚未有人验证协议的匿名性，本文基于Appliedpi

4、演算，讨论了iKP协议是否具有匿名性，同时也验证了它的认证性。关关关键键键词词词安全协议，进程演算，Spi演算，Appliedpi演算，认证性，匿名性3FORMALRESEARCHOFSECURITYPROTOCOLSBASEDONPROCESSCALCULUSABSTRACTWiththewideapplicationandrapiddevelopment，computernet-workisgraduallyacceptedbymanykeydepartments,whichleadstovariousandcomplexrequirementsofsecurity

5、.However,manyexistingsecurityprotocolsareprovennottobesoreliableaswhatwereexpected.Meanwhile,thenetworksystemsstillfaceuptovariousthreatsofneworoldattackingmethods.Thecomplicationofnetworkenvironmentmakestheattackerpossibletolaunchvariousattacksfromthe°awsintheprotocolstobreaknetworksecu

6、rity.Sosecurityprotocolsarecrucialtonetworksecurity.Formalmethodsforprotocolanalysiscanmakethedesignerfocuson,throughsystemanalysis,interfaces,hypothesesoftheenvironment,systemstatesundervariousconditions,exceptionswhensomeconditionsarenotsatis¯edandinvariantproperties.Formalmethodscanal

7、sopro-vide,throughsystemvalidation,guaranteesofsecuritiesofprotocols.Recently,formalmethodsforprotocolanalysisaremainlyofthreekinds:methodsbasedonmodallogicofknowledgeandbelief,methodsbasedontheoremproofandmethodsbasedonprocesscalculus.Amongthemthree,sinceprocesscalculusd