網(wǎng)絡安全認證協(xié)議形式化分析,肖美華南昌大學信息工程學院(南昌,330029)中國科學院軟件研究所計算機科學重點實驗室(北京,100080),2019/12/28,第二十次全國計算機安全學術(shù)交流會,2,Organization,IntroductionRelatedWorkFormalSystemNotationIntrudersAlgorithmicKnowledgeLogicVerificationUsingSPIN/PromelaConclusion,2019/12/28,第二十次全國計算機安全學術(shù)交流會,3,Introduction,Cryptographicprotocolsareprotocolsthatusecryptographytodistributekeysandauthenticateprincipalsanddataoveranetwork.Formalmethods,acombinationofamathematicalorlogicalmodelofasystemanditsrequirements,togetherwithaneffectiveprocedurefordeterminingwhetheraproofthatasystemsatisfiesitsrequirementsiscorrect.Model;Requirement(Specification);Verification.,2019/12/28,第二十次全國計算機安全學術(shù)交流會,4,Introduction(cont.),Incryptographicprotocols,itisverycrucialtoensure:Messagesmeantforaprincipalcannotberead/accessedbyothers(secrecy);Guaranteegenuinenessofthesenderofthemessage(authenticity);Integrity;Non-Repudiation(NRO,NRR);Fairness,etc.,2019/12/28,第二十次全國計算機安全學術(shù)交流會,5,RelatedWork,Techniquesofverifyingsecuritypropertiesofthecryptographicprotocolscanbebroadlycategorized:methodsbasedonbelieflogics(BANLogic)π-calculusbasedmodelsstatemachinemodels(ModelChecking)Modelcheckingadvantages(comparewiththeoryproving):automatic;counterexampleifviolationUseLTL(Lineartemporallogic)tospecifypropertiesFDR(Lowe);Mur?(Mitchell);Interrogator(Millen);Brutus(Marrero)SPIN(Hollzmann)theoremproverbasedmethods(NRL,Meadows)methodsbasedonstatemachinemodelandtheoremprover(Athena,Dawn)TypecheckingISCAS,LOIS,…(inChina),2019/12/28,第二十次全國計算機安全學術(shù)交流會,6,Notation,(1)Messagesa∈Atom::=C|N|k|?m∈Msg::=a|m?m|{m}k(2)ContainRelationship(?)m?a?m=am?m1?m2?m=m1?m2∨m?m1∨m?m2m?{m1}k?m={m1}k∨m?m1Submessage:sub-msgs(m)?{m’∈Msg|m’?m},,,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,7,Notation,(3)Derivation(?,Dolev-Yaomodel)m∈B?B?mB?m∧B?m’?B?m?m’(pairing)B?m?m’?B?m∧B?m’(projection)B?m∧B?k?B?{m}k(encryption)B?{m}k∧B?k-1?B?m(decryption),,,,,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,8,Notation,(4)PropertiesLemma1.B?m∧B?B’?B’?mLemma2.B?m’∧B∪{m’}?m?B?mLemma3.B?m∧X?m∧B?X??（Y:Y∈sub-msgs(m):X?Y∧B?Y）∧?（b:b∈B:Y?b）∧?（Z,k:Z∈Msg∧k∈Key:Y={Z}k∧B?k-1）Lemma4.?（k,b:k∈Key∧b∈B:k?b∧A?k∧A∪B?k）∨?（z:z∈sub-msgs(x):a?z∧A?z）∨?(b:b∈B:a?b∧A?a）,,,,,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,9,LogicofAlgorithmicKnowledge,Definition1.PrimitivepropositionsP0sforsecurity:p,q∈P0s::=sendi(m)Principalisentmessagemrecvi(m)Principalireceivedmessagemhasi(m)Principalihasmessagem,,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,10,LogicofAlgorithmicKnowledge,Definition2.AninterpretedsecuritysystemS=(R,∏R),where∏Risasystemforsecurityprotocols,and∏RisthefollowinginterpretationoftheprimitivepropositionsinR.∏R(r,m)(sendi(m))=trueiff?jsuchthatsend(j,m)∈ri(m)∏R(r,m)(recvi(m))=trueiffrecv(m)∈ri(m)∏R(r,m)(hasi(m))=trueiff?m’suchthatm?m’andrecv(m’)∈ri(m),,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,11,LogicofAlgorithmicKnowledge,Definition3.Aninterpretedalgorithmicsecuritysystem(R,∏R,A1,A2,…,An),whereRisasecuritysystem,and∏RistheinterpretationinR,Aiisaknowledgealgorithmforprincipali.,,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,12,Algorithmknowledgelogic,AiDY(hasi(m),l)?K=keyof(l)foreachrecv(m’)inldoifsubmsg(m,m’,K)thenreturn“Yes”return“No”submsg(m,m’,K)?ifm=m’thenreturntrueifm’is{m1}kandk-1∈Kthenreturnsubmsg(m,m1,K)ifm’ism1.m2thenreturnsubmsg(m,m1,K)∨submsg(m,m2,K)returnfalse,2019/12/28,第二十次全國計算機安全學術(shù)交流會,13,Cont.,getkeys(m,K)?ifm∈Keythenreturn{m}ifm’is{m1}kandk-1∈Kthenreturngetkeys(m1,K)ifm’ism1.m2thenreturngetkeys(m1,K)∪getkeys(m2,K)return{}keysof(l)?K←initkeys(l)loopuntilnochangeinKk←∪getkeys(m,K)(whenrecv(m)∈l)returnK,2019/12/28,第二十次全國計算機安全學術(shù)交流會,14,VerificationUsingSPIN/Promela,SPINisahighlysuccessfulandwidelyusedsoftwaremodel-checkingsystembasedon"formalmethods"fromComputerScience.Ithasmadeadvancedtheoreticalverificationmethodsapplicabletolargeandhighlycomplexsoftwaresystems.InApril2002thetoolwasawardedtheprestigiousSystemSoftwareAwardfor2001bytheACM.SPINusesahighlevellanguagetospecifysystemsdescriptions,includingprotocols,calledPromela(PROcessMEtaLAnguage).,2019/12/28,第二十次全國計算機安全學術(shù)交流會,15,BAN-YahalomProtocol,[1]A→B:A,Na[2]B→S:B,Nb,{A,Na}Kbs[3]S→A:Nb,{B,Kab,Na}Kas,{A,Kab,Nb}Kbs[4]A→B:{A,Kab,Nb}Kbs,{Nb}Kab,2019/12/28,第二十次全國計算機安全學術(shù)交流會,16,Attack1(intruderimpersonatesBobtoAlice),α.1A→I(B):A,Naβ.1I(B)→A:B,Naβ.2A→I(S):A,Na’,{B,Na}Kasγ.2I(A)→S:A,Na,{B,Na}Kasγ.3S→I(B):Na,{A,Kab,Na}Kas,{B,Kab,Na}Kbsα.3I(S)→A:Ne,{B,Kab,Na}Kas,{A,Kab,Na}Kbsα.4A→I(B):{A,Kab,Nb}Kbs,{Ne}Kab,2019/12/28,第二十次全國計算機安全學術(shù)交流會,17,Attack2(intruderimpersonatesAlice),α.1A→B:A,Naα.2B→S:B,Nb,{A,Na}Kbsβ.1I(A)→B:A,(Na,Nb)β.2B→I(S):B,Nb’,{A,Na,Nb}Kasα.3(Omitted)α.4I(A)→B:{A,Na,Nb}Kbs,{Nb}Na,2019/12/28,第二十次全國計算機安全學術(shù)交流會,18,Attack3,α.1A→B:A,Naα.2B→S:B,Nb,{A,Na}Kbsβ.1I(B)→A:B,Nbβ.2A→I(S):A,Na’,{B,Nb}Kasγ.2I(A)→S:A,Na,{B,Nb}Kasβ.3S→I(B):Na,{A,Kab’,Nb}Kbs,{B,Kab’,Na}Kasδ.3I(S)→A:Nb,{B,Kab’,Na}Kas,{A,Kab’,Nb}Kbsα.4A→B:{A,Kab’,Nb}Kbs,{Nb}Kab’,2019/12/28,第二十次全國計算機安全學術(shù)交流會,19,Optimizationstrategies,UsingstaticanalysisandsyntacticalreorderingtechniquesThetwotechniquesareillustratedusingBAN-Yahalomverificationmodelasthebenchmark.describethemodelasOriginalversiontowhichstaticanalysisandthesyntacticalreorderingtechniquesarenotapplied,thestaticanalysistechniqueisonlyusedasFixedversion(1),boththestaticanalysisandthesyntacticalreorderingtechniquesareusedasFixedversion(2).,2019/12/28,第二十次全國計算機安全學術(shù)交流會,20,Experimentalresultsshowtheeffectiveness,2019/12/28,第二十次全國計算機安全學術(shù)交流會,21,Needham-SchroederAuthenticationProtocol,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,22,AttacktoN-SProtocol(foundbySPIN),,,2019/12/28,第二十次全國計算機安全學術(shù)交流會,23,Conclusion,basedonalogicofknowledgealgorithm,aformaldescriptionoftheintrudermodelunderDolev-Yaomodelisconstructed;astudyonverifyingthesecurityprotocolsfollowingaboveusingmodelcheckerSPIN,andthreeattackshavebeenfoundsuccessfullyinonlyonegeneralmodelaboutBAN-Yahalomprotocol;somesearchstrategiessuchasstaticanalysisandsyntacticalreorderingareappliedtoreducethemodelcheckingcomplexityandtheseapproacheswillbenefittheanalysisofmoreprotocols.ScalibilityInanycase,havingalogicwherewecanspecifytheabilitiesofintrudersisanecessaryprerequisitetousingmodel-checkingtechniques.,2019/12/28,第二十次全國計算機安全學術(shù)交流會,24,,Thanks!,