特殊环境下的协议安全研究

上海交通大学硕士学位论文特殊环境下的协议安全研究姓名：高长喆申请学位级别：硕士专业：计算机系统结构指导教师：陈克非20070101InternetGSPML-TLS----THERESEARCHOFSECURITYPROTOCOLSINSPECIALENVIRONMENTABSTRACTWiththedevelopmentofInternettechnology,securityprotocolsplaymoreandmoreimportantine-businessande-governmentapplication.Peoplepaymoreattentiononthesecurityofprotocols,especiallyinhowtomodelandanalyzesecurityprotocolsinspecialenvironment.Wefirstresearchandanalyzeontheexistingmodelingandanalyzingmethodsonsecurityprotocolsandfindtheadvantagesanddisadvantagesofthem.Consideringthespecialityoftheenvironment,wechooseevent-basedGSPMLlanguagetosetupvisualmodelsforgeneralchallenge-responseprotocolandthesimplifiedversionofTLShandshakeprotocol,whichmeetalloutstandards.Thenwegiveadetailanalysisonthesecurityconditionsforgeneralchallenge-responseprotocol,andwelistthenecessaryconditionsforchallenge-responseprotocolinbothsymmetryandasymmetrycryptographicforms,aswellastheattacktothemiftheconditionsarenotmet.Thepointweshouldpayattentiontoisthedifferencebetweentheminimumformsofbothcryptographicforms.Afterthat,weanalyzethetraditionalthreeroundsauthenticationprotocolsandfindthatthepureauthenticationprotocolcannotachieveitsgoalintheenvironmentwithactiveintruders.Besidesthat,fourautomationtoolsofformalmethodsareanalyzedinthispaper.Thesetoolscontainthelogic,modelcheckingandprovingmethods.Wecomparethesetoolsfromuserinterfaceandusability,numberofrunningstatsandtime,thesupportofdataindependenceanddiscretetimemodeling,abilityoferrorchecking,anddrawaresultonthecomprehensiveabilitiesofthem.KEYWORDS:securityprotocol,formalmethod,automationtool,challenge-responseprotocol1GPSML·························································································62BAN·······················································93·············································································104-····························191·············································································402··············································································413··························································424······································································425······················································43CSPConcurrentSequentialProcessFDRFailureDivergenceRefinementSPEARSecurityProtocolEngineeringandAnalysisResourceSyMPSymbolicModelProverSPASecurityProtocolAnalysisDASSDistributedAuthenticationSecurityServiceUMLUnifiedModelingLanguageMDAModelDrivenAchitectureCPALCommonProtocolAnalysisLanguage–58–2007127–59–20071272007127–1–11.11.1.11.1.21978Needham-SchroederDenningSacco[2]Lowe[3]–2–1.1.31.2[21]--–3–-1.3-TLS--TLSOtway-ReesDenning-SaccoDSSA–4–22.12.1.1[4]MDAMDAUML2.0[5]UML2.0MDAJ.McDermott[6]MDAMDAUMLUMLUMLUMLUMLgCSP2.1.2–5–McDermottGuizzardi[7]MAMAGuizzardi[7]MAAMGuizzardi[7]MAAMGuizzardi[7]MAMAUMLUML2.1.3GSPMLGSPMLGSPMLGSPML–6–GSPML[30]McDermott[6]Yahahlom[8]Dolev-YaoGSPMLGSPMLGSPMLGSPMLGSPML1GPSML2.22.2.1eventregionprocessregionsequentialboxconcurrentbox–7–AknowsPAbelievesPIfyouknowP,thenPistrueTTruePPSyverson[9]BANBAN[8][11][12][9]Kailar[13]KindredRV[14]1BANBurrowsAbadiNeedhamBANBANBANBurrowsBANbelievingseeingcontrolingsayingmessageBANBANBAN1234BAN1–8–2341C2C1C2CBAN12342BAN–9–2BAN2BANBANBANGNY[11]AT[12]SVO[9][10]GNYATBANSVOAT2.2.2FDRMurφNRLInterrogatorProtocolInitializeInitialassumptionSessionmessagesDerivingbyBANlogicSecuritygoalTheprotocolisnotsecureTheprotocolissecure–10–1231CSPCSPC.A.R.Hoare[HORA04]CSPCSPCSPCSPCSPCSPCSP12DescriptionofsecurityprotocolsFormalizedprotocolsIntrudermodelAnalyzerErrorfinding.–11–CSP1NETM≠↑≠⇒↑•∀mUSERintrmUSERouttrMNET.0....0.:msat2PbaPsatAUTH(tr)≠↑≠⇒↑=atrbtrtrAUTH)(CSPBA−AB2KemmererInaJo[SCHO88]Murφ[1]2.2.31997ThayerHerzongGuttman[41][THG99b]∑*()A±∑*()A→±∑[SYVE01]1.s,i,s∈∑i1(())ilengthtrs≤≤N(s,i)s–12–2.(,)nsiN=∈index(n)=i,strand(n)=s.term(n)=(())itrs,si2_()((()))iunstermntrs=si3.12,nnN∈12nn→1()termna=+2()termna=−aA∈1na2na4.12(,),(,1)nsiNnsiN=∈=+∈12nn⇒1n2ns'nn+⇒'nn5.n12nn→12nn⇒,()N→⇒U,,,()cccccCN→⊆→⇒⊆⇒=→⇒U,()N→⇒UC1.C2.2cnN∈2()termn1cnN∈12cnn→3.2cnN∈12nn⇒12cnn⇒4.CS()S⊆→⇒UspSspSspspssNN×sNSGuttman[42]SongAthena[39]Athena[40]Athena[41]AthenaAthenaAthenaAthenaAthenaAthenaAthena[39]2–13–initfinalsplit[40]Athena2.32.3.1SPEARSPEARSPEAEII1997SPEARISPEARIISPEARIIGYPIEGNYVisualGNYPrologGNYGYNGERGYNERPrologGNYGNYGNYGYNGERPrologGNYGNYGNY[15]2.3.2MurϕMurφ[1]MurφMurφMurφMurφMurφC++MurφMurφMurφTMNKerverosV5Murφ1–14–2345MurφMurφFDRMurφa).b).2.3.3FDRFDRCSP-Hoare[16][17]CSPCSPCSP1Tracesrefinement)()(^PtracesQtracesQPT⊆=⊆2Failurerefinement)()(^PfailuresQfailuresQPF⊆=⊆3-Failure-Divergencerefinement)()()()(^PsdivergenceQsdivergencePfailuresQfailuresQPFD⊆∧⊆=⊆–15–TracesFFD2.3.4SyMPSyMp[38]-SergeyBerezinSyMPSyMPAthenaSML.sympAthenaDawnSongAthena.athsendreceive[39]Athenainit(;)PΓ−∆l−∆finall∆splitpruningsplitpruningprune_keys:–16–prune_signed:SyMPSMLEmacsUnix/Linux2.4UMLGSPMLGSPML-TLS–17–33.13.1.1[18]CA-1233.1.2–18–3.2-3.2.1--P1P:AB−:1C2P:BA−:12,RC3P:AB−:2R1CABBA1R2CAB2R1R2RABBA-C.Mitchell[19]-Nnatualfo