基于有向图的网络协议建模 毕业设计论文

《基于有向图的网络协议建模 毕业设计论文》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、摘要网络协议是互联网通信的基本构架，不完备或错误的协议往往给攻击者提供了攻击的机会。因为协议本身的高并发性以及所处环境的复杂性，网络协议的设计是非常困难的。我们可以通过对协议设计完毕后进行安全建模，并进行自动化验证，来找到协议设计存在的安全隐患。在本文中，我们用两种方法分别对BGP协议进行建模。方法一基于规则推理，对协议进行完全分析，得到协议资源和具有某种推导关系的行为，基本资源可以作为协议行为的参数，通过用AND和OR来表示协议行为的推导关系。将此方法应用到BGP协议，最终在BGP协议的攻击规则图上得到了29条攻击路径。方法二用CSP对协议

2、建模，用CSP来表示协议之间各个进程的并发作用，模型包括协议本身、攻击者，以及所要满足的安全约束。并用FDR检验所建立的模型是否满足约束。用该方法来对BGP进行建模验证，检验结果为，该模型满足其中一个约束，而另一个没有被满足的约束得到了一个反例序列。本文提出了两种对协议进行分析以及建模的方法，一种是基于规则的，一种是用形式化的方法来进行建模。通过这两种方法，我们可以用建立的模型来准确的描述网络协议，使得更好的理解网络协议，并通过对协议的有效分析与验证，得到协议的攻击方法与协议的缺陷。关键词：CSP；网络协议；规则；安全建模；BGP协议4ABS

3、TRACTNetworkprotocolisthebasicframeworkofInternetcommunications,however,theincompleteorincorrectprotocoloftenprovidesattackerssomeopportunities.Becauseofthehighconcurrencyofanetworkprotocolandthecomplexityoftheenvironmentwhereitworks,itisdifficulttodesignanetworkprotocolwit

4、hareliablesafety.Wecanfindoutanetworkpotential’ssafetyhazardthroughsecuritymodelingandautomatedverification.Inthispaper,we’llusetwomethodstomodelontheBGPprotocol.Thefirstmethodbasesontherule-basedreasoningapproachtoanalyzetheprotocolandgetprotocolresourcesaswellasbehaviorsw

5、hichhavesomekindsofderivedrelations.Thebasicresourcesserveastheparametersoftheprotocol’sbehaviorsandindicatesthederivedrelationsby“AND”and“OR”.ApplyingthismethodtoBGPprotocol,wesuccessfullyget29attackpathsontheattackingrulesdiagram.ThesecondmethodistomodelwithCSP.We’lluseCS

6、Ptoindicatetheconcurrencyeffectofeveryprocessamongtheprotocols.Thismodelcontainsnotonlytheprotocolsbutalsotheattackersandthesecurityconstraintswhichneedtobesatisfied.Atthesametime,weuseFDRtotestthismodeltoexamwhetheritmeetstheconstraints.Inthisway,wetestifytheBGPandtheresul

7、tisthatoneofthetwoconstraintsissatisfiedwhiletheotherisunsatisfiedfromwhichwegetacounter-examplesequence.Weproposetwomethods---oneisrule-based,theotherisformalized---tomodelandanalyzetheprotocol.Byusingthemodel,weareabletopreciselydescribethenetworkprotocol,andthendeepenthe

8、comprehensionofit.Byanalyzingtheprotocolefficientlyandtesting,weobtainthetypesofat