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

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

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

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

【部分圖文】：

轉(zhuǎn)換過程

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

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


本文編號(hào)：2939112