网络安全认证协议形式化分析课件(PPT 24页).pptx

1、网络安全认证协议形式化分析第1页，共24页。Organization nIntroductionnRelated WorknFormal System NotationnIntruders Algorithmic Knowledge LogicnVerification Using SPIN/PromelanConclusion 2022-7-242第2页，共24页。Introduction nCryptographic protocols are protocols that use cryptography to distribute keys and authenticate princ

2、ipals and data over a network.nFormal methods,a combination of a mathematical or logical model of a system and its requirements,together with an effective procedure for determining whether a proof that a system satisfies its requirements is correct.Model;Requirement(Specification);Verification.2022-

3、7-243第3页，共24页。Introduction(cont.)In cryptographic protocols,it is very crucial to ensure:Messages meant for a principal cannot be read/accessed by others(secrecy);Guarantee genuineness of the sender of the message(authenticity);Integrity;Non-Repudiation(NRO,NRR);Fairness,etc.2022-7-244第4页，共24页。Relat

4、ed WorkTechniques of verifying security properties of the cryptographic protocols can be broadly categorized:nmethods based on belief logics(BAN Logic)n-calculus based models n state machine models(Model Checking)Model checking advantages(compare with theory proving):automatic;counterexample if viol

5、ation Use LTL(Linear temporal logic)to specify properties FDR(Lowe);Mur(Mitchell);Interrogator(Millen);Brutus(Marrero)SPIN(Hollzmann)n theorem prover based methods(NRL,Meadows)n methods based on state machine model and theorem prover(Athena,Dawn)nType checkingnISCAS,LOIS,(in China)2022-7-245第5页，共24页

6、。Notation(1)Messages a Atom:=C|N|k|m Msg:=a|m m|mk(2)Contain Relationship()m a m=a m m1 m2 m=m1 m2 m m1 m m2 m m1k m=m1k m m1 Submessage:sub-msgs(m)m Msg|m m 2022-7-246第6页，共24页。Notation(3)Derivation(,Dolev-Yao model)m B B m B m B m B m m (pairing)B m m B m B m (projection)B m B k B mk (encryption)B

7、mk B k-1 B m (decryption)2022-7-247第7页，共24页。Notation(4)Properties Lemma 1.B m B B B m Lemma 2.B m B m m B m Lemma 3.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=Zk B k-1）Lemma 4.（k,b:k Key b B:k b A k AB k）（z:z sub-msgs(x):a z A z）(b:b B:a b A a）2022-7-248第8页，共24页。Logic of Algo

8、rithmic KnowledgeDefinition 1.Primitive propositions P0s for security:p,q P0s:=sendi(m)Principal i sent message m recvi(m)Principal i received message m hasi(m)Principal i has message m 2022-7-249第9页，共24页。Logic of Algorithmic KnowledgeDefinition 2.An interpreted security system S=(R,R),where R is a

9、system for security protocols,and R is the following interpretation of the primitive propositions in R.R(r,m)(sendi(m)=true iff j such that send(j,m)ri(m)R(r,m)(recvi(m)=true iff recv(m)ri(m)R(r,m)(hasi(m)=true iff m such that m m and recv(m)ri(m)2022-7-2410第10页，共24页。Logic of Algorithmic KnowledgeDe

10、finition 3.An interpreted algorithmic security system (R,R,A1,A2,An),where R is a security system,and R is the interpretation in R,Ai is a knowledge algorithm for principal i.2022-7-2411第11页，共24页。Algorithm knowledge logic AiDY(hasi(m),l)K=keyof(l)for each recv(m)in l do if submsg(m,m,K)then return“Y

11、es”return“No”submsg(m,m,K)if m=m then return true if m is m1k and k-1 K then return submsg(m,m1,K)if m is m1.m2 then return submsg(m,m1,K)submsg(m,m2,K)return false2022-7-2412第12页，共24页。Cont.getkeys(m,K)if m Key then return m if m is m1k and k-1 K then return getkeys(m1,K)if m is m1.m2 then return ge

12、tkeys(m1,K)getkeys(m2,K)return keysof(l)K initkeys(l)loop until no change in K k getkeys(m,K)(when recv(m)l)return K2022-7-2413第13页，共24页。Verification Using SPIN/PromelaSPIN is a highly successful and widely used software model-checking system based on formal methods from Computer Science.It has made

13、 advanced theoretical verification methods applicable to large and highly complex software systems.In April 2002 the tool was awarded the prestigious System Software Award for 2001 by the ACM.SPIN uses a high level language to specify systems descriptions,including protocols,called Promela(PROcess M

14、Eta LAnguage).2022-7-2414第14页，共24页。BAN-Yahalom Protocol 1 AB:A,Na 2 BS:B,Nb,A,NaKbs 3 SA:Nb,B,Kab,NaKas,A,Kab,NbKbs 4 AB:A,Kab,NbKbs,NbKab2022-7-2415第15页，共24页。Attack 1(intruder impersonates Bob to Alice).1 AI(B):A,Na .1 I(B)A:B,Na .2 AI(S):A,Na,B,NaKas .2 I(A)S:A,Na,B,NaKas .3 SI(B):Na,A,Kab,NaKas,B

15、,Kab,NaKbs.3 I(S)A:Ne,B,Kab,NaKas,A,Kab,NaKbs.4 AI(B):A,Kab,NbKbs,NeKab 2022-7-2416第16页，共24页。Attack 2(intruder impersonates Alice).1 AB:A,Na.2 BS:B,Nb,A,NaKbs .1 I(A)B:A,(Na,Nb).2 BI(S):B,Nb,A,Na,NbKas.3 (Omitted).4 I(A)B:A,Na,NbKbs,NbNa 2022-7-2417第17页，共24页。Attack 3.1 AB:A,Na.2 BS:B,Nb,A,NaKbs .1 I

16、(B)A:B,Nb .2 AI(S):A,Na,B,NbKas .2 I(A)S:A,Na,B,NbKas .3 SI(B):Na,A,Kab,NbKbs,B,Kab,NaKas .3 I(S)A:Nb,B,Kab,NaKas,A,Kab,NbKbs.4 AB:A,Kab,NbKbs,NbKab2022-7-2418第18页，共24页。Optimization strategies nUsing static analysis and syntactical reordering techniquesnThe two techniques are illustrated using BAN-Y

17、ahalom verification model as the benchmark.ndescribe the model as Original version to which static analysis and the syntactical reordering techniques are not applied,nthe static analysis technique is only used as Fixed version(1),nboth the static analysis and the syntactical reordering techniques ar

18、e used as Fixed version(2).2022-7-2419第19页，共24页。Experimental results show the effectivenessProtocol Model ConfigurationWith type flawsNo type flawsStatesTrans.StatesTrans.Original version15802065549697Fixed version(1)7121690405379Fixed version(2)433512225 2432022-7-2420第20页，共24页。Needham-Schroeder Au

19、thentication Protocol 2022-7-2421第21页，共24页。Attack to N-S Protocol(found by SPIN)2022-7-2422第22页，共24页。Conclusion(1)based on a logic of knowledge algorithm,a formal description of the intruder model under Dolev-Yao model is constructed;(2)a study on verifying the security protocols following above usi

20、ng model checker SPIN,and three attacks have been found successfully in only one general model about BAN-Yahalom protocol;(3)some search strategies such as static analysis and syntactical reordering are applied to reduce the model checking complexity and these approaches will benefit the analysis of more protocols.(4)ScalibilityIn any case,having a logic where we can specify the abilities of intruders is a necessary prerequisite to using model-checking techniques.2022-7-2423第23页，共24页。Thanks!2022-7-2424第24页，共24页。