網絡安全認證協(xié)議形式化分析-文庫吧
2024-12-24 23:45 本頁面
【正文】 over 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） ∨ ?（ z: z ∈ submsgs(x) : a ? z ∧ A ? z） ∨ ? (b: b ∈ B: a ? b∧ A ? a） ? ?2022/2/5 第二十次全國計算機安全學術交流會 9 Logic of Algorithmic Knowledge Definition 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 m ?2022/2/5 第二十次全國計算機安全學術交流會 10 Logic of Algorithmic Knowledge Definition 2. An interpreted security sy
試題試卷相關推薦
鄂ICP備17016276號-1