次全国计算机安全学术交流会.ppt

《次全国计算机安全学术交流会.ppt》由会员分享，可在线阅读，更多相关《次全国计算机安全学术交流会.ppt（24页珍藏版）》请在装配图网上搜索。

网络安全认证协议形式化分析,肖美华南昌大学信息工程学院(南昌,330029)中国科学院软件研究所计算机科学重点实验室(北京,100080),2019/12/28,第二十次全国计算机安全学术交流会,2,Organization,IntroductionRelatedWorkFormalSystemNotationIntrudersAlgorithmicKnowledgeLogicVerificationUsingSPIN/PromelaConclusion,2019/12/28,第二十次全国计算机安全学术交流会,3,Introduction,Cryptographicprotocolsareprotocolsthatusecryptographytodistributekeysandauthenticateprincipalsanddataoveranetwork.Formalmethods,acombinationofamathematicalorlogicalmodelofasystemanditsrequirements,togetherwithaneffectiveprocedurefordeterminingwhetheraproofthatasystemsatisfiesitsrequirementsiscorrect.Model;Requirement(Specification);Verification.,2019/12/28,第二十次全国计算机安全学术交流会,4,Introduction(cont.),Incryptographicprotocols,itisverycrucialtoensure:Messagesmeantforaprincipalcannotberead/accessedbyothers(secrecy);Guaranteegenuinenessofthesenderofthemessage(authenticity);Integrity;Non-Repudiation(NRO,NRR);Fairness,etc.,2019/12/28,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,9,LogicofAlgorithmicKnowledge,Definition1.PrimitivepropositionsP0sforsecurity:p,q∈P0s::=sendi(m)Principalisentmessagemrecvi(m)Principalireceivedmessagemhasi(m)Principalihasmessagem,,,2019/12/28,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,11,LogicofAlgorithmicKnowledge,Definition3.Aninterpretedalgorithmicsecuritysystem(R,∏R,A1,A2,…,An),whereRisasecuritysystem,and∏RistheinterpretationinR,Aiisaknowledgealgorithmforprincipali.,,,2019/12/28,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,14,VerificationUsingSPIN/Promela,SPINisahighlysuccessfulandwidelyusedsoftwaremodel-checkingsystembasedon"formalmethods"fromComputerScience.Ithasmadeadvancedtheoreticalverificationmethodsapplicabletolargeandhighlycomplexsoftwaresystems.InApril2002thetoolwasawardedtheprestigiousSystemSoftwareAwardfor2001bytheACM.SPINusesahighlevellanguagetospecifysystemsdescriptions,includingprotocols,calledPromela(PROcessMEtaLAnguage).,2019/12/28,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,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,第二十次全国计算机安全学术交流会,19,Optimizationstrategies,UsingstaticanalysisandsyntacticalreorderingtechniquesThetwotechniquesareillustratedusingBAN-Yahalomverificationmodelasthebenchmark.describethemodelasOriginalversiontowhichstaticanalysisandthesyntacticalreorderingtechniquesarenotapplied,thestaticanalysistechniqueisonlyusedasFixedversion(1),boththestaticanalysisandthesyntacticalreorderingtechniquesareusedasFixedversion(2).,2019/12/28,第二十次全国计算机安全学术交流会,20,Experimentalresultsshowtheeffectiveness,2019/12/28,第二十次全国计算机安全学术交流会,21,Needham-SchroederAuthenticationProtocol,,2019/12/28,第二十次全国计算机安全学术交流会,22,AttacktoN-SProtocol(foundbySPIN),,,2019/12/28,第二十次全国计算机安全学术交流会,23,Conclusion,basedonalogicofknowledgealgorithm,aformaldescriptionoftheintrudermodelunderDolev-Yaomodelisconstructed;astudyonverifyingthesecurityprotocolsfollowingaboveusingmodelcheckerSPIN,andthreeattackshavebeenfoundsuccessfullyinonlyonegeneralmodelaboutBAN-Yahalomprotocol;somesearchstrategiessuchasstaticanalysisandsyntacticalreorderingareappliedtoreducethemodelcheckingcomplexityandtheseapproacheswillbenefittheanalysisofmoreprotocols.ScalibilityInanycase,havingalogicwherewecanspecifytheabilitiesofintrudersisanecessaryprerequisitetousingmodel-checkingtechniques.,2019/12/28,第二十次全国计算机安全学术交流会,24,,Thanks!,