時(shí)態(tài)認(rèn)知邏輯的模型檢測與安全協(xié)議驗(yàn)證.pdf

1、本文主要針對時(shí)態(tài)認(rèn)知邏輯的模型檢測問題進(jìn)行了初步研究，研究成果體現(xiàn)在如下幾方面：(1)論文首先對安全協(xié)議驗(yàn)證的形式化方法進(jìn)行了概括和總結(jié)。并討論了今后安全協(xié)議驗(yàn)證的一些研究方向。安全協(xié)議驗(yàn)證的形式化方法主要包括模型檢測、定理證明、petri網(wǎng)方法、pi演算方法、csp(CommunicatingSequentialProcesses)方法和串空間方法等。從基本原理、方法及工具到在安全協(xié)議驗(yàn)證的應(yīng)用等方面比較詳細(xì)的討論了計(jì)算機(jī)專家們在形式

2、化方法方面所做的工作。(2)在SMV(SymbolicModelVerification)等模型檢測工具的基礎(chǔ)上，根據(jù)知識的語義和集合理論，提出了多智體系統(tǒng)時(shí)態(tài)認(rèn)知邏輯模型檢測方法。使SMV等模型檢測工具的功能從時(shí)態(tài)邏輯擴(kuò)展到時(shí)態(tài)認(rèn)知邏輯。而時(shí)態(tài)認(rèn)知邏輯己被廣泛應(yīng)用于分布式系統(tǒng)和協(xié)議的規(guī)范描述。本文也以TMN(MTatebayashi，NMatsuzaki，DBNewman)協(xié)議為例，探討了該算法在安全協(xié)議驗(yàn)證方面的應(yīng)用。(3)根據(jù)自動(dòng)

3、機(jī)理論和知識的語義，提出了“Onthefly”模型檢測時(shí)態(tài)認(rèn)知規(guī)范的算法，該算法在模型檢測帶有知識算子的時(shí)態(tài)規(guī)范時(shí)，往往只需產(chǎn)生系統(tǒng)的小部分狀態(tài)空間，就能找到一個(gè)反例，從而實(shí)現(xiàn)“Onthefly”模型檢測時(shí)態(tài)認(rèn)知規(guī)范，且算法的時(shí)間復(fù)雜性是多項(xiàng)式時(shí)間的。算法也以TMN協(xié)議為例，探討了該算法在安全協(xié)議驗(yàn)證方面的應(yīng)用。(4)通過協(xié)議行為結(jié)構(gòu)的定義，及對行為和行為結(jié)構(gòu)的分析，提出了一種新的密碼協(xié)議秘密性的驗(yàn)證算法，該算法的時(shí)間復(fù)雜度是多項(xiàng)式時(shí)間