如今中國已經(jīng)進入了一個互聯(lián)網(wǎng)+的時代,各行各業(yè)都搭上了互聯(lián)網(wǎng)的快車。安全協(xié)議作為一個關(guān)系到互聯(lián)網(wǎng)流通的信息安全的重要因素,變得舉足輕重。目前分析協(xié)議的方法多種多樣,模型檢測作為一種形式化方法受到廣泛關(guān)注和認可。本文在前人建模、驗證的基礎(chǔ)上,擴展出反例分析階段。試圖從反例角度出發(fā),從反例中提取有效信息,通過分析反例來定位漏洞位置。模型檢測方法具有兩個主要的優(yōu)點:第一,模型檢測具有高度的自動化,可以使研究者從繁雜的搜索任務(wù)中解脫出來。第二,當系統(tǒng)或者協(xié)議不滿足約定的性質(zhì)時,模型檢測工具可以返回一個源碼級別的事件序列,既反例。但是隨著功能的增加和完善,現(xiàn)有的系統(tǒng)和協(xié)議變得越來越復(fù)雜,與之對應(yīng)的反例數(shù)量越來越多,內(nèi)容也越來越復(fù)雜,因此對反例的分析也變得越來越困難。本文提出了消除眾多相似反例的方法。在使用模型檢測器對協(xié)議進行驗證時候,我們發(fā)現(xiàn)會有大量的相似反例,他們體現(xiàn)了同一個安全漏洞,但我們僅僅需要一個此類的反例,過多的反例只會增加系統(tǒng)負擔(dān),給分析反例的過程帶來干擾。本文通過引入節(jié)點權(quán)重方法來在反例生成時消除相似反例。為了保證去重效果又增加了反例生成后的消除過程。以此來保證反例集合中沒有相似反... 

【文章來源】：電子科技大學(xué)四川省 211工程院校 985工程院校 教育部直屬院校

【文章頁數(shù)】：88 頁

【學(xué)位級別】：碩士

【部分圖文】：

轉(zhuǎn)換過程

圖2-1 轉(zhuǎn)換過程2.1.2 CTL分支時序邏輯圖2-2 常用CTL運算符CTL（Computation Tree Logic）分支時序邏輯是CTL*計算樹邏輯的一個子集，該子集受到一些限制：其中每個時序運算符X、F、G、U和R必須由一個路徑量詞

第二章 安全協(xié)議分析相關(guān)理論領(lǐng)。在很大程度上說，CTL是CTL*由以下路徑公式語法規(guī)則來代替CTL*中則而得到的子集：如果f和g是狀態(tài)公式，那么Xf、Ff、Gf、fUg和fRg是路徑公圖2-2描述來了四種基本的CTL運算符：M，0 EF g、M，0 AF g、 MEG g、 M，0 AG g。1.3 LTL線性時態(tài)邏輯線性時態(tài)邏輯[22-23]（LTL，Linear Temporal Logic）包括具有形為Af的公式中f是路徑公式，它的狀態(tài)子公式只允許為原子命題。如下圖2-4表示了LTL運。更準確的說，LTL路徑公式為以下兩種：（1）如果p ∈ AP'，則p為路徑公式。（2）如果F和g是路徑公式，則 f、f∨g、f∧g、X f、F f、G f、f U G和f 路徑公式。


本文編號：2939112