基于術(shù)語(yǔ)猜測(cè)及Hash偽造的安全協(xié)議自動(dòng)化驗(yàn)證.pdf

1、南京航空航天大學(xué)碩士學(xué)位論文基于術(shù)語(yǔ)猜測(cè)及Hash偽造的安全協(xié)議自動(dòng)化驗(yàn)證姓名：吳燕申請(qǐng)學(xué)位級(jí)別：碩士專業(yè)：計(jì)算機(jī)應(yīng)用技術(shù)指導(dǎo)教師：章勇20061201南京航空航天大學(xué)碩士學(xué)位論文VAbstractThesecurityprotocolsprovidesecurityservicesfthewkinfmationexchangearethefoundationofthewksecurity.Howevertheintrudercanim

2、plementvariousattacksusingflawsofsecurityprotocols’own.Whetherthesecurityprotocolsaresafebecomesthemostcriticalproblem.Earlieranalyzingbyartificialprovingisextremelyfallible.Theexaminationscopeisalsotoonarrow.Itisurgentt

3、odesignmebelievablefmalizeanalysismethods.Thispaperproposesthevalidatinglogicffmllyanalyzingsecurityprotocols.Thismethodhasimprovementsabouttwoimptantaspects:fmalizingprotocolsdesigningintrudermodel.Iteffectivelyovercome

4、stheflowsoflogicalproofmethodbasingonthebeliefitcannotonlyfindtheattackbutalsoprovethesecurityofprotocols.ThispaperalsoproposesakindofexpansionintrudermodelwithapplyingthetheiesabouttermguessingHashcollisions.Termguessin

5、gisthenewhotspotinprotocolanalysisresearchrecentyears.HashcollisionistheuptodatesignificantbreakthroughaboutcryptologybasingonwhichweproposeHashfgefthefirsttime.Duetotheseexpansionsourmethodhasfoundmeattacks.Thispapergiv

6、essomeusefulcommentsabouthowtoeffectivelyavoidthesenewkindsofattacks.Furthermethispaperanalyzestwoimptantkindofprotocols——ecommerceprotocolthesecuritysocketlevelprotocol.Attheendweimplementasecurityprotocolsautomatically

7、analysissystembasingonthevalidatinglogicintrudermodelproposeddesignaprotocolspecificationlanguage.Wefirsttimeproposethedesignthoughtthatclassificatingthespecificationlanguagewhileimplementing.Comparingwithcurrenttoolsour

8、systemcananalyzemetypesfindmeflowprovemecredibly.AccdingtheresultwesearchedtheguessingattackofWooLamΠ4theHashfgeattackofMSCHAPv2haveneverfoundbefe.Ourresearchisreferrenceftheverifyingdesigningofsecurityprotocolsevenfthes