网络安全认证协议形式化分析.ppt

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