網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析(已修改)
2025-01-20 23:45 本頁(yè)面
【正文】 網(wǎng)絡(luò)安全認(rèn)證協(xié)議形式化分析 肖 美 華 南昌大學(xué)信息工程學(xué)院 (南昌 ,330029) 中國(guó)科學(xué)院軟件研究所計(jì)算機(jī)科學(xué)重點(diǎn)實(shí)驗(yàn)室 (北京 ,100080) 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 2 Organization ? Introduction ? Related Work ? Formal System Notation ? Intruders Algorithmic Knowledge Logic ? Verification Using SPIN/Promela ? Conclusion 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 3 Introduction ? Cryptographic protocols are protocols that use 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。 Requirement (Specification)。 Verification. 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 4 Introduction (cont.) In cryptographic protocols, it is very crucial to ensure: Messages meant for a principal cannot be read/accessed by others (secrecy)。 Guarantee genuineness of the sender of the message (authenticity)。 Integrity。 NonRepudiation (NRO, NRR)。 Fairness, etc. 2022/2/5 第二十次全國(guó)計(jì)算機(jī)安全學(xué)術(shù)交流會(huì) 5 Related Work Techniques of verifying security properties of the cryptographic protocols can be broadly categorized: ? methods based on belief logics (BAN Logic) ? πcalculus based models ? state machine models (Model Checking) Model checking advantages (pare 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) ? theorem pr
試題試卷相關(guān)推薦
鄂ICP備17016276號(hào)-1