《次全国计算机安全学术交流会.ppt》由会员分享，可在线阅读，更多相关《次全国计算机安全学术交流会.ppt（24页珍藏版）》请在金锄头文库上搜索。
1、网络安全认证协议形式化分析肖肖 美美 华华南昌大学信息工程学院南昌大学信息工程学院( (南昌南昌,330029),330029)中国科学院软件研究所计算机科学重点实验室中国科学院软件研究所计算机科学重点实验室( (北京北京,100080),100080)Organization nIntroductionnRelated WorknFormal System NotationnIntruders Algorithmic Knowledge LogicnVerification Using SPIN/PromelanConclusion 7/25/20242第二十次全国计算机安全学术交流会第二十
2、次全国计算机安全学术交流会 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 procedure for
3、determining whether a proof that a system satisfies its requirements is correct. Model; Requirement (Specification);Verification. 7/25/20243第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会 Introduction (cont.)In cryptographic protocols, it is very crucial to ensure:Messages meant for a principal cannot be read/acce
4、ssed by others (secrecy);Guarantee genuineness of the sender of the message (authenticity);Integrity;Non-Repudiation (NRO, NRR);Fairness, etc. 7/25/20244第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Related WorkTechniques of verifying security properties of the cryptographic protocols can be broadly categorized:n
5、methods 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 (Linear temporal logic ) to specify properties FDR (Lowe); Mur (Mitchell); Interrogator (M
6、illen); 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)7/25/20245第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Notation(1) Messages a Atom := C | N | k | m Msg := a | m m |
7、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 7/25/20246第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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 mk B
8、k-1 B m (decryption) 7/25/20247第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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）
9、(b: b B: a b A a） 7/25/20248第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Logic 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 message m7/25/20249第二十次全国计算机安全学术交流会第二十次全
10、国计算机安全学术交流会Logic 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) (recvi (m) = tr
11、ue iff recv(m) ri (m) R(r, m) (hasi (m) = true iff m such that m m and recv(m ) ri (m)7/25/202410第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Logic 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,
12、 Ai is a knowledge algorithm for principal i. 7/25/202411第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Algorithm 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(
13、m, m1, K) if m is m1 .m2 then return submsg(m, m1, K) submsg(m, m2, K) return false7/25/202412第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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 getkeys(m1, K) getkeys(m2, K) return keysof(l) K initkey
14、s(l) loop until no change in K k getkeys(m, K) (when recv(m) l ) return K7/25/202413第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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 advanced theoretica
15、l 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 MEta LAnguage).
16、7/25/202414第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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 , NbKab7/25/202415第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Attack 1 (intruder impersonates Bob to Alice).1 AI(B): A, Na .1 I(B)A: B, Na .2 AI(S): A, Na
17、, 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 7/25/202416第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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
18、): B, Nb, A, Na, NbKas .3 (Omitted).4 I(A)B: A, Na, NbKbs , NbNa 7/25/202417第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Attack 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,
19、 NbKbs.4 AB: A, Kab, NbKbs , NbKab7/25/202418第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Optimization 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
20、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).7/25/202419第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Experimental results
21、show the effectivenessProtocol Model ConfigurationWith type flawsNo type flawsStatesTrans.StatesTrans.Original version15802065549697Fixed version(1)7121690405379Fixed version(2)433512225 2437/25/202420第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会Needham-Schroeder Authentication Protocol 7/25/202421第二十次全国计算机安全学术交
22、流会第二十次全国计算机安全学术交流会Attack to N-S Protocol (found by SPIN)7/25/202422第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会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
23、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. 7/25/202423第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会 Thanks!7/25/202424第二十次全国计算机安全学术交流会第二十次全国计算机安全学术交流会
