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

1、2/24/2022编辑编辑ppt1网络安全认证协议形式化分析肖肖 美美 华华南昌大学信息工程学院南昌大学信息工程学院( (南昌南昌,330029),330029)中国科学院软件研究所计算机科学重点实验室中国科学院软件研究所计算机科学重点实验室( (北京北京,100080),100080)2/24/2022编辑编辑ppt2Organization nIntroductionnRelated WorknFormal System NotationnIntruders Algorithmic Knowledge LogicnVerification Using SPIN/PromelanConclu

2、sion 2/24/2022编辑编辑ppt3 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 logical model of a system and its requirements, together with an effective proce

3、dure for determining whether a proof that a system satisfies its requirements is correct. Model; Requirement (Specification);Verification. 2/24/2022编辑编辑ppt4 Introduction (cont.)In cryptographic protocols, it is very crucial to ensure:Messages meant for a principal cannot be read/accessed by others (

4、secrecy);Guarantee genuineness of the sender of the message (authenticity);Integrity;Non-Repudiation (NRO, NRR);Fairness, etc. 2/24/2022编辑编辑ppt5Related WorkTechniques of verifying security properties of the cryptographic protocols can be broadly categorized:nmethods based on belief logics (BAN Logic

5、)n-calculus based models n state machine models (Model Checking) Model checking advantages (compare 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)

6、n theorem prover based methods (NRL, Meadows)n methods based on state machine model and theorem prover (Athena, Dawn)nType checkingnISCAS, LOIS, (in China)2/24/2022编辑编辑ppt6Notation(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 m

7、2 m m1k m = m1k m m1 Submessage: sub-msgs(m) m Msg | m m 2/24/2022编辑编辑ppt7Notation(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 mk B k-1 B m (decryption) 2/24/2022编辑编辑ppt8Notation(4) Properties Lemma 1. B m B B B m Lemma 2.

8、 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） 2/24/2022编辑编辑ppt9Logic of Algorithmic KnowledgeDefinition 1. Primitive propositions P0s for secur

9、ity: p, q P0s := sendi (m) Principal i sent message m recvi (m) Principal i received message m hasi (m) Principal i has message m 2/24/2022编辑编辑ppt10Logic of Algorithmic KnowledgeDefinition 2. An interpreted security system S = (R, R), where R is a system for security protocols, and R is the followin

10、g 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) 2/24/2022编辑编辑ppt11Logic of Algorithmic KnowledgeDefinition 3. An interpreted

11、 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. 2/24/2022编辑编辑ppt12Algorithm 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

12、 “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 false2/24/2022编辑编辑ppt13Cont.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

13、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 K2/24/2022编辑编辑ppt14Verification Using SPIN/PromelaSPIN is a highly successful and widely used software model-checking system based on formal methods from Computer Sc

14、ience. 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 specify systems descriptions, including protocols, ca

15、lled Promela (PROcess MEta LAnguage). 2/24/2022编辑编辑ppt15BAN-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 , NbKab2/24/2022编辑编辑ppt16Attack 1 (intruder impersonates Bob to Alice).1 AI(B): A, Na .1 I(B)A: B, Na .2 AI(S): A, Na, B, NaKas .

16、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 2/24/2022编辑编辑ppt17Attack 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

17、 I(A)B: A, Na, NbKbs , NbNa 2/24/2022编辑编辑ppt18Attack 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, Kab, NbKbs , B, Kab, NaKas .3 I(S)A: Nb, B, Kab, NaKas , A, Kab, NbKbs.4 AB: A, Kab, NbKbs , NbKab2/24/2022编辑编辑ppt19Optimizati

18、on strategies nUsing static analysis and syntactical reordering techniquesnThe two techniques are illustrated using BAN-Yahalom 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

19、analysis technique is only used as Fixed version(1),nboth the static analysis and the syntactical reordering techniques are used as Fixed version(2).2/24/2022编辑编辑ppt20Experimental results show the effectivenessProtocol Model ConfigurationWith type flawsNo type flawsStatesTrans.StatesTrans.Original version15802065549697Fixed version(1)7121690405379Fixed version(2)433512225 2432/24/2022编辑编辑ppt21Needham-Schroeder Authentication Protocol 2/24/2022编辑编辑ppt22Attack to N-S Protocol (found by SPIN)2/24/2022编辑编辑ppt23Conclusionnbased on a logic of kn