- 相關(guān)推薦
符號化模型檢測網(wǎng)絡(luò )安全協(xié)議
畢業(yè)論文
摘 要
簡(jiǎn)要回顧了形式化方法的發(fā)展歷程,闡述了形式化分析的定義、方法、重要性及主要研究?jì)热?討論了形式規約語(yǔ)言與方法,以及演繹證明和模型檢測等形式化驗證方法。
密碼協(xié)議安全性的分析是網(wǎng)絡(luò )安全的1個(gè)難題,運用形式化方法對密碼協(xié)議進(jìn)行分析1直是該領(lǐng)域的研究熱點(diǎn)；本文以1個(gè)實(shí)例闡述運用模型檢測工具ＳＭＶ對ＴＭＮ密碼協(xié)議進(jìn)行形式分析,在建立1個(gè)有限狀態(tài)系統模型和刻畫(huà)ＴＭＮ密碼協(xié)議安全性質(zhì)的基礎上,發(fā)現了1些新的攻擊。
著(zhù)重分析了模型檢測技術(shù)和邏輯推證技術(shù)的優(yōu)點(diǎn)和不足,并在此基礎上提出了1種混合形式化技術(shù)的說(shuō)明,該技術(shù)可提供更為完全的安全協(xié)議形式化分析。
關(guān)鍵字：形式化分析；SMV模型；模型檢測；邏輯推證；混合分析技術(shù)。
Abstract
This paper presents the definition and importance of formal methods after simply looking back on the history of formal methods, and provides an overview of formal methods. Discusses specification languages (methods) and verification methods that include deductive proving and model checking.
It is a hard problem in area of computer network security to analyze cryptographic protocols. Using formal methods to analyze cryptographic protocols remains the key issue in this field. In this paper, a methodology is presented by using a model checker of formal methods, SMV, to analyze the TMN cryptographic protocol. After building a finite state system of the protocol and describing the security property of the protocol, SMV is used to discover some new attacks upon TMN cryptographic protocol.
The advantages and disadvantages of model checking technology and logic reasoning technology is analyzed, Based on it, the author gives a specification of new mixed technology of the two technologies which can provide a more complete formal analysis of security protocols.
Key words： formal analysis; SMV; model checking; logic reasoning technology; mixed formal analysis technology.
注釋?zhuān)翰缓创a
【符號化模型檢測網(wǎng)絡(luò )安全協(xié)議】相關(guān)文章：
談分布式入侵檢測系統模型設計09-04
淺談分布式入侵檢測系統模型設計07-11
基于A(yíng)daBoost+膚色模型的多人臉檢測考勤系統06-01
淺談平面廣告信息傳達的符號化09-06
淺談平面廣告信息傳達的符號化06-03
剩余收益模型與傳統DCF模型的比較研究07-07
運動(dòng)模型與Ad Hoc路由協(xié)議性能仿真08-01
消費社會(huì )的女性符號化傾向-淺析“美女經(jīng)濟＂的社會(huì )學(xué)透視09-01
論IP電話(huà)模型09-13
審計風(fēng)險模型探討08-26