網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析(存儲版)
【正文】 se cryptography to distribute keys and authenticate principals and data over a work. ? Formal methods, a bination of a mathematical or logical 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。 Mur? (Mitchell)。 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 第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會 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 第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會 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 第二十次全國計(jì)算機(jī)安全學(xué)術(shù)交流會 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 第二
試題試卷相關(guān)推薦
鄂ICP備17016276號-1