網絡安全認證協(xié)議形式化分析(參考版)
2025-01-11 23:45本頁面
【正文】 (3) some search strategies such as static analysis and syntactical reordering are applied to reduce the model checking plexity and these approaches will benefit the analysis of more protocols. (4) Scalibility In any case, having a logic where we can specify the abilities of intruders is a necessary prerequisite to using modelchecking techniques. 2022/2/5 第二十次全國計算機安全學術交流會 24 Thanks! 。 Brutus (Marrero) SPIN (Hollzmann) ? theorem prover based methods (NRL, Meadows) ? methods based on state machine model and theorem prover (Athena, Dawn) ? Type checking ? ISCAS, LOIS, …(in China) 2022/2/5 第二十次全國計算機安全學術交流會 6 Notation (1) Messages a ∈ Atom ::= C | N | k | ? m ∈ Msg ::= a | m? m | {m}k (2) Contain Relationship (?) m ? a ? m = a m ? m1? m2 ? m = m1? m2 ∨ m ? m1∨ m ? m2 m ? {m1}k ? m = {m1}k ∨ m ? m1 Submessage: submsgs(m) ? {m’ ∈ Msg | m’ ? m } ?2022/2/5 第二十次全國計算機安全學術交流會 7 Notation (3) Derivation (?, DolevYao 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 ? {m}k (encryption) B ? {m}k ∧ B ? k1 ? B ? m (decryption) ? ?2022/2/5 第二十次全國計算機安全學術交流會 8 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 ∈ submsgs(m) : X ? Y∧ B ? Y） ∧ ?（ b: b ∈ B : Y ? b） ∧ ?（ Z, k: Z ∈ Msg ∧ k ∈ Key : Y = {Z}k ∧ B ? k1） Lemma 4. ?（ k, b: k ∈ Key ∧ b ∈ B : k ? b ∧ A ? k ∧ A∪ B ? k） ∨
試題試卷相關推薦
鄂ICP備17016276號-1