基于術(shù)語猜測及Hash偽造的安全協(xié)議自動化驗證.pdf

1、南京航空航天大學(xué)碩士學(xué)位論文基于術(shù)語猜測及Hash偽造的安全協(xié)議自動化驗證姓名：吳燕申請學(xué)位級別：碩士專業(yè)：計算機(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