網絡安全認證協(xié)議形式化分析ppt課件

1、網絡安全認證協(xié)議形式化分析肖肖 美美 華華(,330029)(,330029)( (北京北京,100080),100080)1;.2022-2-9;.2Organization nIntroductionnRelated WorknFormal System NotationnIntruders Algorithmic Knowledge LogicnVerification Using SPIN/PromelanConclusion 2022-2-9;.3 Introduction nCryptographic protocols are protocols that use cryptog

2、raphy to distribute keys and authenticate principals 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. n

3、Model; nRequirement (Specification);Verification. 2022-2-9;.4 Introduction (cont.)In cryptographic protocols, it is very crucial to ensure:nMessages meant for a principal cannot be read/accessed by others (secrecy);nGuarantee genuineness of the sender of the message (authenticity);nIntegrity;nNon-Re

4、pudiation (NRO, NRR);Fairness, etc. 2022-2-9;.5Related 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 (compa

5、re with theory proving): automatic; counterexample if violation 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 p

6、rover (Athena, Dawn)nType checkingnISCAS, LOIS, (in China)2022-2-9;.6Notation(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-2-9;.7Notation(3) Derivation ( , Dolev-Y

7、ao 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 mk B k-1 B m (decryption) 2022-2-9;.8Notation(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）

8、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-2-9;.9Logic of Algorithmic 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

9、message m 2022-2-9;.10Logic of Algorithmic KnowledgeDefinition 2. An interpreted security system S = (R, R), where R is a 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) (rec

10、vi (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-2-9;.11Logic of Algorithmic KnowledgeDefinition 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

11、algorithm for principal i. 2022-2-9;.12Algorithm knowledge logic AiDY(hasi(m),l) K = keyof(l) for each recv(m) in l do if submsg(m, m, K) then return “Yes” 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,

12、 K) submsg(m, m2, K) return false2022-2-9;.13Cont.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 getkeys(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-2-9

13、;.14Verification Using SPIN/PromelaSPIN is a highly successful and widely used software model-checking system based on formal methods from Computer Science. It has made advanced theoretical verification methods applicable to large and highly complex software systems. In April 2002 the tool was award

14、ed 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 MEta LAnguage). 2022-2-9;.15BAN-Yahalom Protocol 1 AB: A, Na 2 BS: B, Nb, A, NaKbs 3 SA: Nb, B, Kab, NaKas , A, Kab, NbKbs 4 AB:

15、 A, Kab, NbKbs , NbKab2022-2-9;.16Attack 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, Kab, NaKbs.3 I(S)A: Ne, B, Kab, NaKas , A, Kab, NaKbs.4 AI(B): A, Kab, NbKbs , NeKab 2022-2-9;.17Attack

16、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-2-9;.18Attack 3.1 AB: A, Na.2 BS: B, Nb, A, NaKbs .1 I(B)A: B, Nb .2 AI(S): A, Na, B, NbKas .2 I(A)S: A, Na, B, NbKas .3 SI(B): Na, A,

17、Kab, NbKbs , B, Kab, NaKas .3 I(S)A: Nb, B, Kab, NaKas , A, Kab, NbKbs.4 AB: A, Kab, NbKbs , NbKab2022-2-9;.19Optimization strategies nUsing static analysis and syntactical reordering techniquesnThe two techniques are illustrated using BAN-Yahalom verification model as the benchmark.ndescribe the mo

18、del 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 are used as Fixed version(2).2022-2-9;.20Experimental result

19、s show the effectivenessProtocol Model ConfigurationWith type flawsNo type flawsStatesTrans.StatesTrans.Original version15802065549697Fixed version(1)7121690405379Fixed version(2)433512225 2432022-2-9;.21Needham-Schroeder Authentication Protocol 2022-2-9;.22Attack to N-S Protocol (found by SPIN)2022-2-9;.23Conclusionnbased on a logic of knowledge algori