網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析課件

網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析2021/6/101網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析2021/6/101OrganizationIntroductionRelatedWorkFormalSystemNotationIntrudersAlgorithmicKnowledgeLogicVerificationUsingSPIN/PromelaConclusion2021/6/102OrganizationIntroduction2021/Introduction

Cryptographicprotocolsareprotocolsthatusecryptographytodistributekeysandauthenticateprincipalsanddataoveranetwork.Formalmethods,acombinationofamathematicalorlogicalmodelofasystemanditsrequirements,togetherwithaneffectiveprocedurefordeterminingwhetheraproofthatasystemsatisfiesitsrequirementsiscorrect.Model;Requirement(Specification);Verification.

2021/6/103Introduction2021/6/103Introduction

(cont.)Incryptographicprotocols,itisverycrucialtoensure:Messagesmeantforaprincipalcannotberead/accessedbyothers(secrecy);Guaranteegenuinenessofthesenderofthemessage(authenticity);Integrity;Non-Repudiation(NRO,NRR);Fairness,etc.

2021/6/104Introduction(cont.)IncryptoRelatedWorkTechniquesofverifyingsecuritypropertiesofthecryptographicprotocolscanbebroadlycategorized:methodsbasedonbelieflogics(BANLogic)π-calculusbasedmodelsstatemachinemodels(ModelChecking)

Modelcheckingadvantages(comparewiththeoryproving):automatic;counterexampleifviolationUseLTL(Lineartemporallogic)tospecifyproperties

FDR(Lowe);Mur(Mitchell);

Interrogator(Millen);Brutus(Marrero)

SPIN(Hollzmann)theoremproverbasedmethods(NRL,Meadows)methodsbasedonstatemachinemodelandtheoremprover(Athena,Dawn)TypecheckingISCAS,LOIS,…(inChina)2021/6/105RelatedWorkTechniquesofveriNotation(1)Messages

a

∈Atom::=C|N|k|

m

∈

Msg::=a|m?

m|{m}k(2)Contain

Relationship(?)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}

2021/6/106Notation(1)Messages2021/6/106Notation(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)2021/6/107Notation(3)Derivation(?,DolNotation(4)

Properties

Lemma1.

B?m∧B?B’?B’?m

Lemma2.B?m’∧B∪{m’}?m?B?m

Lemma3.

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）2021/6/108Notation(4)Properties2021/6LogicofAlgorithmicKnowledgeDefinition1.PrimitivepropositionsP0sforsecurity:p,q∈

P0s::=sendi(m)Principalisentmessagemrecvi(m)Principalireceivedmessagemhasi(m)Principalihasmessagem2021/6/109LogicofAlgorithmicKnowledgeLogicofAlgorithmicKnowledgeDefinition2.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))=trueiffm’suchthatm?m’andrecv(m’)∈

ri(m)2021/6/1010LogicofAlgorithmicKnowledgeLogicofAlgorithmicKnowledgeDefinition3.Aninterpretedalgorithmicsecuritysystem(R,∏R,A1,A2,…,An),whereRisasecuritysystem,and∏RistheinterpretationinR,Aiisaknowledgealgorithmforprincipali.

2021/6/1011LogicofAlgorithmicKnowledgeAlgorithmknowledgelogic

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)returnfalse2021/6/1012AlgorithmknowledgelogicAiDYCont.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)returnK2021/6/1013Cont.getkeys(m,K)?ifm∈KeVerificationUsingSPIN/PromelaSPINisahighlysuccessfulandwidelyusedsoftwaremodel-checkingsystembasedon"formalmethods"fromComputerScience.Ithasmadeadvancedtheoreticalverificationmethodsapplicabletolargeandhighlycomplexsoftwaresystems.InApril2002thetoolwasawardedtheprestigiousSystemSoftwareAwardfor2001bytheACM.SPINusesahighlevellanguagetospecifysystemsdescriptions,includingprotocols,calledPromela(PROcessMEtaLAnguage).

2021/6/1014VerificationUsingSPIN/PromelBAN-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}Kab2021/6/1015BAN-YahalomProtocol2021/6/10Attack1

(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

2021/6/1016Attack1(intruderimpersonateAttack2

(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

2021/6/1017Attack2(intruderimpersonateAttack3α.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’2021/6/1018Attack3α.1A→B:A,Na2021/6/Optimizationstrategies

UsingstaticanalysisandsyntacticalreorderingtechniquesThetwotechniquesareillustratedusingBAN-Yahalomverificationmodelasthebenchmark.describethemodelasOriginalversiontowhichstaticanalysisandthesyntacticalreorderingtechniquesarenotapplied,thestaticanalysistechniqueisonlyusedasFixedversion(1),boththestaticanalysisandthesyntacticalreorderingtechniquesareusedasFixedversion(2).2021/6/1019Optimizationstrategies2021ExperimentalresultsshowtheeffectivenessProtocolModelConfigurationWithtypeflawsNotypeflawsStatesTrans.StatesTrans.Originalversion15802065549697Fixedversion(1)7121690405379Fixedversion(2)4335122252432021/6/1020ExperimentalresultsshowtheNeedham-SchroederAuthenticationProtocol

2021/6/1021Needham-SchroederAuthenticatiAttacktoN-SProtocol(foundbySPIN)2021/6/1022AttacktoN-SProtocol(foundConclusionbasedonalogicofknowledgealgorithm,aformaldescriptionoftheintrudermodelunderDolev-Yaomodelisconstructed;astudyonverifyingthesecurityprotocolsfollowingaboveusingmodelcheckerSPIN,andthreeattackshavebeenfoundsuccessfullyinonlyonegeneralmodelaboutBAN-Yahalomprotocol;somesearchstrategiessuchasstaticanalysisandsyntacticalreorderingareappliedtoreducethemodelcheckingcomplexityandtheseapproacheswillbenefittheanalysisofmoreprotocols.ScalibilityInanycase,havingalogicwherewecanspecifytheabilitiesofintrudersisanecessaryprerequisitetousingmodel-checkingtechniques.

2021/6/1023Conclusionbasedonalogicof

Thanks!2021/6/10242021/6/1024問(wèn)題解答?2021/6/1025問(wèn)題解答?2021/6/1025網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析2021/6/1026網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析2021/6/101OrganizationIntroductionRelatedWorkFormalSystemNotationIntrudersAlgorithmicKnowledgeLogicVerificationUsingSPIN/PromelaConclusion2021/6/1027OrganizationIntroduction2021/Introduction

Cryptographicprotocolsareprotocolsthatusecryptographytodistributekeysandauthenticateprincipalsanddataoveranetwork.Formalmethods,acombinationofamathematicalorlogicalmodelofasystemanditsrequirements,togetherwithaneffectiveprocedurefordeterminingwhetheraproofthatasystemsatisfiesitsrequirementsiscorrect.Model;Requirement(Specification);Verification.

2021/6/1028Introduction2021/6/103Introduction

(cont.)Incryptographicprotocols,itisverycrucialtoensure:Messagesmeantforaprincipalcannotberead/accessedbyothers(secrecy);Guaranteegenuinenessofthesenderofthemessage(authenticity);Integrity;Non-Repudiation(NRO,NRR);Fairness,etc.

2021/6/1029Introduction(cont.)IncryptoRelatedWorkTechniquesofverifyingsecuritypropertiesofthecryptographicprotocolscanbebroadlycategorized:methodsbasedonbelieflogics(BANLogic)π-calculusbasedmodelsstatemachinemodels(ModelChecking)

Modelcheckingadvantages(comparewiththeoryproving):automatic;counterexampleifviolationUseLTL(Lineartemporallogic)tospecifyproperties

FDR(Lowe);Mur(Mitchell);

Interrogator(Millen);Brutus(Marrero)

SPIN(Hollzmann)theoremproverbasedmethods(NRL,Meadows)methodsbasedonstatemachinemodelandtheoremprover(Athena,Dawn)TypecheckingISCAS,LOIS,…(inChina)2021/6/1030RelatedWorkTechniquesofveriNotation(1)Messages

a

∈Atom::=C|N|k|

m

∈

Msg::=a|m?

m|{m}k(2)Contain

Relationship(?)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}

2021/6/1031Notation(1)Messages2021/6/106Notation(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)2021/6/1032Notation(3)Derivation(?,DolNotation(4)

Properties

Lemma1.

B?m∧B?B’?B’?m

Lemma2.B?m’∧B∪{m’}?m?B?m

Lemma3.

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）2021/6/1033Notation(4)Properties2021/6LogicofAlgorithmicKnowledgeDefinition1.PrimitivepropositionsP0sforsecurity:p,q∈

P0s::=sendi(m)Principalisentmessagemrecvi(m)Principalireceivedmessagemhasi(m)Principalihasmessagem2021/6/1034LogicofAlgorithmicKnowledgeLogicofAlgorithmicKnowledgeDefinition2.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))=trueiffm’suchthatm?m’andrecv(m’)∈

ri(m)2021/6/1035LogicofAlgorithmicKnowledgeLogicofAlgorithmicKnowledgeDefinition3.Aninterpretedalgorithmicsecuritysystem(R,∏R,A1,A2,…,An),whereRisasecuritysystem,and∏RistheinterpretationinR,Aiisaknowledgealgorithmforprincipali.

2021/6/1036LogicofAlgorithmicKnowledgeAlgorithmknowledgelogic

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)returnfalse2021/6/1037AlgorithmknowledgelogicAiDYCont.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)returnK2021/6/1038Cont.getkeys(m,K)?ifm∈KeVerificationUsingSPIN/PromelaSPINisahighlysuccessfulandwidelyusedsoftwaremodel-checkingsystembasedon"formalmethods"fromComputerScience.Ithasmadeadvancedtheoreticalverificationmethodsapplicabletolargeandhighlycomplexsoftwaresystems.InApril2002thetoolwasawardedtheprestigiousSystemSoftwareAwardfor2001bytheACM.SPINusesahighlevellanguagetospecifysystemsdescriptions,includingprotocols,calledPromela(PROcessMEtaLAnguage).

2021/6/1039VerificationUsingSPIN/PromelBAN-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}Kab2021/6/1040BAN-YahalomProtocol2021/6/10Attack1

(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

2021/6/1041Attack1(intruderimpersonateAttack2

(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

2021/6/1042Attack2(intruderimpersonateAttack3α.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’2021/6/1043Attack3α.1A→B:A,Na2021/6/Optimizationstrate