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

1、2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)會(huì)1網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析肖肖 美美 華華南昌大學(xué)信息工程學(xué)院南昌大學(xué)信息工程學(xué)院( (南昌南昌,330029),330029)中國科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)重點(diǎn)實(shí)驗(yàn)室中國科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)重點(diǎn)實(shí)驗(yàn)室( (北京北京,100080),100080)2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)2Organization nIntroductionnRelated WorknFormal System NotationnIntruders Algorithmic Know

2、ledge LogicnVerification Using SPIN/PromelanConclusion 2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)3 Introduction nCryptographic protocols are protocols that use cryptography to distribute keys and authenticate principals and data over a network.nFormal methods, a combination of a mathematical or logic

3、al 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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)4 Introduction (cont.)In cryptographic protoc

4、ols, 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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)5Related WorkTechniques of verif

5、ying 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 violation Use LTL (Linea

6、r 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-2-18第二十次全國計(jì)算機(jī)安全

7、學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)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-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)7Notation(3) Derivation ( , Dolev-Yao model) m B B m

8、 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-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)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 :

9、 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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)9Logic of Algorithmic KnowledgeDefinition 1. Primitive propositions P0s for security: p, q P0s := sendi (m) Principal i sent message m recvi (m) Principal i

10、 received message m hasi (m) Principal i has message m 2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)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

11、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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)11Logic of Algorithmic KnowledgeDefinition 3. An interpreted algorithmic security sys

12、tem (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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)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

13、 “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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)13Cont.getkeys(m, K) if m Key then return m if m is m1k and k-1 K then return getkeys(m1

14、, 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-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)14Verification Using SPIN/PromelaSPIN is a highly successful and widely used software model-checki

15、ng 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 awarded the prestigious System Software Award for 2001 by the ACM. SPIN uses a high level language to spe

16、cify systems descriptions, including protocols, called Promela (PROcess MEta LAnguage). 2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)15BAN-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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)16Atta

17、ck 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-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)17Attack 2 (intr

18、uder 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-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)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,

19、 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-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)19Optimization strategies nUsing static analysis and syntactical reordering techniquesnThe two techniques are illustrated using BAN-Yahal

20、om 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 are u

21、sed as Fixed version(2).2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)20Experimental results show the effectivenessProtocol Model ConfigurationWith type flawsNo type flawsStatesTrans.StatesTrans.Original version15802065549697Fixed version(1)7121690405379Fixed version(2)433512225 2432022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)21Needham-Schroeder Authentication Protocol 2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)22Attack to N-S Protocol (found by SPIN)2022-2-18第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會(huì)