1摘要网络协议是互联网通信的基本构架,不完备或错误的协议往往给攻击者提供了攻击的机会。因为协议本身的高并发性以及所处环境的复杂性,网络协议的设计是非常困难的。我们可以通过对协议设计完毕后进行安全建模,并进行自动化验证,来找到协议设计存在的安全隐患。在本文中,我们用两种方法分别对BGP协议进行建模。方法一基于规则推理,对协议进行完全分析,得到协议资源和具有某种推导关系的行为,基本资源可以作为协议行为的参数,通过用AND和OR来表示协议行为的推导关系。将此方法应用到BGP协议,最终在BGP协议的攻击规则图上得到了29条攻击路径。方法二用CSP对协议建模,用CSP来表示协议之间各个进程的并发作用,模型包括协议本身、攻击者,以及所要满足的安全约束。并用FDR检验所建立的模型是否满足约束。用该方法来对BGP进行建模验证,检验结果为,该模型满足其中一个约束,而另一个没有被满足的约束得到了一个反例序列。本文提出了两种对协议进行分析以及建模的方法,一种是基于规则的,一种是用形式化的方法来进行建模。通过这两种方法,我们可以用建立的模型来准确的描述网络协议,使得更好的理解网络协议,并通过对协议的有效分析与验证,得到协议的攻击方法与协议的缺陷。关键词:CSP;网络协议;规则;安全建模;BGP协议2ABSTRACTNetworkprotocolisthebasicframeworkofInternetcommunications,however,theincompleteorincorrectprotocoloftenprovidesattackerssomeopportunities.Becauseofthehighconcurrencyofanetworkprotocolandthecomplexityoftheenvironmentwhereitworks,itisdifficulttodesignanetworkprotocolwithareliablesafety.Wecanfindoutanetworkpotential'ssafetyhazardthroughsecuritymodelingandautomatedverification.Inthispaper,we'llusetwomethodstomodelontheBGPprotocol.Thefirstmethodbasesontherule-basedreasoningapproachtoanalyzetheprotocolandgetprotocolresourcesaswellasbehaviorswhichhavesomekindsofderivedrelations.Thebasicresourcesserveastheparametersoftheprotocol'sbehaviorsandindicatesthederivedrelationsby"AND"and"OR".ApplyingthismethodtoBGPprotocol,wesuccessfullyget29attackpathsontheattackingrulesdiagram.ThesecondmethodistomodelwithCSP.We'lluseCSPtoindicatetheconcurrencyeffectofeveryprocessamongtheprotocols.Thismodelcontainsnotonlytheprotocolsbutalsotheattackersandthesecurityconstraintswhichneedtobesatisfied.Atthesametime,weuseFDRtotestthismodeltoexamwhetheritmeetstheconstraints.Inthisway,wetestifytheBGPandtheresultisthatoneofthetwoconstraintsissatisfiedwhiletheotherisunsatisfiedfromwhichwegetacounter-examplesequence.Weproposetwomethods---oneisrule-based,theotherisformalized---tomodelandanalyzetheprotocol.Byusingthemodel,weareabletopreciselydescribethenetworkprotocol,andthendeepenthecomprehensionofit.Byanalyzingtheprotocolefficientlyandtesting,weobtainthetypesofa