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

网络安全认证协议形式化分析,肖美华南昌大学信息工程学院(南昌,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)MessagesaAtom:=C|N|k|mMsg:=a|mm|mk(2)ContainRelationship()mam=amm1m2m=m1m2mm1mm2mm1km=m1kmm1Submessage:sub-msgs(m)mMsg|mm,2019/12/28,第二十次全国计算机安全学术交流会,7,Notation,(3)Derivation(,Dolev-Yaomodel)mBBmBmBmBmm(pairing)BmmBmBm(projection)BmBkBmk(encryption)BmkBk-1Bm(decryption),2019/12/28,第二十次全国计算机安全学术交流会,8,Notation,(4)PropertiesLemma1.BmBBBmLemma2.BmBmmBmLemma3.BmXmBX（Y:Ysub-msgs(m):XYBY）（b:bB:Yb）（Z,k:ZMsgkKey:Y=ZkBk-1）Lemma4.（k,b:kKeybB:kbAkABk）（z:zsub-msgs(x):azAz）(b:bB:abAa）,2019/12/28,第二十次全国计算机安全学术交流会,9,LogicofAlgorithmicKnowledge,Definition1.PrimitivepropositionsP0sforsecurity:p,qP0s:=sendi(m)Principalisentmessagemrecvi(m)Principalireceivedmessagemhasi(m)Principalihasmessagem,2019/12/28,第二十次全国计算机安全学术交流会,10,LogicofAlgorithmicKnowledge,Definition2.AninterpretedsecuritysystemS=(R,R),whereRisasystemforsecurityprotocols,andRisthefollowinginterpretationoftheprimitivepropositionsinR.R(r,m)(sendi(m)=trueiffjsuchthatsend(j,m)ri(m)R(r,m)(recvi(m)=trueiffrecv(m)ri(m)R(r,m)(hasi(m)=trueiffmsuchthatmmandrecv(m)ri(m),2019/12/28,第二十次全国计算机安全学术交流会,11,LogicofAlgorithmicKnowledge,Definition3.Aninterpretedalgorithmicsecuritysystem(R,R,A1,A2,An),whereRisasecuritysystem,andRistheinterpretationinR,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=mthenreturntrueifmism1kandk-1Kthenreturnsubmsg(m,m1,K)ifmism1.m2thenreturnsubmsg(m,m1,K)submsg(m,m2,K)returnfalse,2019/12/28,第二十次全国计算机安全学术交流会,13,Cont.,getkeys(m,K)ifmKeythenreturnmifmism1kandk-1Kthenreturngetkeys(m1,K)ifmism1.m2thenreturngetkeys(m1,K)getkeys(m2,K)returnkeysof(l)Kinitkeys(l)loopuntilnochangeinKkgetkeys(m,K)(whenrecv(m)l)returnK,2019/12/28,第二十次全国计算机安全学术交流会,14,VerificationUsingSPIN/Promela,SPINisahighlysuccessfulandwidelyusedsoftwaremodel-checkingsystembasedonformalmethodsfromComputerScience.Ithasmadeadvancedtheoreticalverificationmethodsapplicabletolargeandhighlycomplexsoftwaresystems.InApril2002thetoolwasawardedtheprestigiousSystemSoftwareAwardfor2001bytheACM.SPINusesahighlevellanguagetospecifysystemsdescriptions,includingprotocols,calledPromela(PROcessMEtaLAnguage).,2019/12/28,第二十次全国计算机安全学术交流会,15,BAN-YahalomProtocol,1AB:A,Na2BS:B,Nb,A,NaKbs3SA:Nb,B,Kab,NaKas,A,Kab,NbKbs4AB:A,Kab,NbKbs,NbKab,2019/12/28,第二十次全国计算机安全学术交流会,16,Attack1(intruderimpersonatesBobtoAlice),.1AI(B):A,Na.1I(B)A:B,Na.2AI(S):A,Na,B,NaKas.2I(A)S:A,Na,B,NaKas.3SI(B):Na,A,Kab,NaKas,B,Kab,NaKbs.3I(S)A:Ne,B,Kab,NaKas,A,Kab,NaKbs.4AI(B):A,Kab,NbKbs,NeKab,2019/12/28,第二十次全国计算机安全学术交流会,17,Attack2(intruderimpersonatesAlice),.1AB:A,Na.2BS:B,Nb,A,NaKbs.1I(A)B:A,(Na,Nb).2BI(S):B,Nb,A,Na,NbKas.3(Omitted).4I(A)B:A,Na,NbKbs,NbNa,2019/12/28,第二十次全国计算机安全学术交流会,18,Attack3,.1AB:A,Na.2BS:B,Nb,A,NaKbs.1I(B)A:B,Nb.2AI(S):A,Na,B,NbKas.2I(A)S:A,Na,B,NbKas.3SI(B):Na,A,Kab,NbKbs,B,Kab,NaKas.3I(S)A:Nb,B,Kab,NaKas,A,Kab,NbKbs.4AB:A,Kab,NbKbs,NbKab,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!,