网络安全认证协议形式化分析资料教程.ppt

网络安全认证协议形式化分析资料教程.ppt网络安全认证协议形式化分析肖美华南昌大学信息工程学院(南昌,330029)中国科学院软件研究所计算机科学重点实验室(北京,100080)*anizationIntroductionRelatedWorkFormalSystemNotationIntrudersAlgorithmicKnowledgeLogicVerificationUsingSPIN/,acombinationofamathematicalorlogicalmodelofasystemanditsrequirements,;Requirement(Specification);:methodsbasedonbelieflogics(BANLogic)π-calculusbasedmodelsstatemachinemodels(ModelChecking)parewiththeoryproving):automatic;counterexampleifviolationUseLTL(Lineartemporallogic)tospecifypropertiesFDR(Lowe);Mur(Mitchell);Interrogator(Millen);Brutus(Marrero)SPIN(Hollzmann)theoremproverbasedmethods(NRL,Meadows)methodsbasedonstatemachinemodelandtheoremprover(Athena,Dawn)TypecheckingISCAS,LOIS,…(inChina)Date5第二十次全国计算机安全学术交流会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}Date6第二十次全国计算机安全学术交流会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)Date7第二十次全国计算机安全学术交流会Notation(4)⊦m∧B⊆B’⇒B’⊦⊦m’∧B∪{m’}⊦m⇒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):p,q∈P0s::=sendi(m)Principalisentmessagemrecvi(m)Principalireceivedmessagemhasi(m)=(R,∏R),where∏Risasystemforsecurityprotocols,and∏RisthefollowinginterpretationoftheprimitivepropositionsinR.∏R(r,m)(sendi(m))=trueiffjsuchthatsend(j,m)∈ri(m)∏R