基于CP-nets模型的安全協(xié)議形式化方法研究.pdf

1、隨著計(jì)算機(jī)網(wǎng)絡(luò)的迅速發(fā)展，信息通信的安全問題變得越來(lái)越突出，越來(lái)越復(fù)雜，解決安全問題對(duì)許多網(wǎng)絡(luò)應(yīng)用來(lái)說(shuō)具有重要意義。目前，網(wǎng)絡(luò)通信安全問題的解決方案中，安全協(xié)議是最有效的手段之一。由于網(wǎng)絡(luò)本身的開放性，使得網(wǎng)絡(luò)中存在著各種安全威脅，攻擊者可以采用多種方式對(duì)安全協(xié)議進(jìn)行攻擊，破壞其安全屬性。分析安全協(xié)議中可能存在的缺陷很難完全由人工來(lái)識(shí)別，因此，需要借助形式化的分析方法和工具來(lái)完成。
　　安全協(xié)議的形式化分析過(guò)程包含安全協(xié)議系統(tǒng)建模

2、、安全屬性驗(yàn)證、以及攻擊序列生成等。本文通過(guò)分析安全協(xié)議模型中攻擊者的“任意”性行為和協(xié)議的多次并發(fā)會(huì)話問題，提出了一種改進(jìn)的攻擊者模型和多并發(fā)會(huì)話劃分分析方法。針對(duì)安全屬性驗(yàn)證和攻擊序列生成問題，采用安全屬性違背事件對(duì)不安全狀態(tài)進(jìn)行分類描述，提出基于安全屬性違背事件生成攻擊序列的兩種方法:狀態(tài)空間搜索法和on-the-fly生成方法?；诎踩珜傩赃`背事件生成攻擊序列的方法能夠有效地控制搜索范圍，提高搜索效率。最后通過(guò)分析安全協(xié)議中的數(shù)

3、據(jù)特征，提取能夠構(gòu)成攻擊的攻擊策略，并依據(jù)攻擊策略確定攻擊目的，構(gòu)建基于攻擊目的的模型，選擇生成攻擊序列，有效地削減安全協(xié)議模型檢測(cè)的狀態(tài)空間。
　　本文的貢獻(xiàn)和創(chuàng)新性工作如下:
　　(1)提出安全協(xié)議模型的多并發(fā)會(huì)話劃分分析方法
　　針對(duì)帶有攻擊者模型的安全協(xié)議形式化模型的復(fù)雜運(yùn)行特點(diǎn)，提出一種改進(jìn)的攻擊者模型。通過(guò)對(duì)Dolev-Yao攻擊者模型進(jìn)行分析，將攻擊者的功能劃分為分解和合成兩個(gè)前后階段。同時(shí)，分析帶有攻擊

4、者的安全協(xié)議形式化模型時(shí)，往往需要考慮多次并發(fā)會(huì)話的情況下攻擊是否成功的情況。文本針對(duì)這一特點(diǎn)，通過(guò)會(huì)話配置和會(huì)話順序的設(shè)定，提出多并發(fā)會(huì)話劃分分析方法，一次分析一種并發(fā)情況，能夠有效地劃分并削減模型驗(yàn)證的狀態(tài)空間。
　　(2)提出基于安全屬性違背事件的安全協(xié)議攻擊序列生成方法
　　針對(duì)攻擊序列生成需求，定義面向安全協(xié)議攻擊序列生成的CP-nets模型(Attack Trace Generation Oriented CP-

5、nets，ATG-CPN)。依據(jù)安全協(xié)議規(guī)范和模型的特點(diǎn)，給出安全屬性的形式化定義，并將攻擊狀態(tài)采用安全屬性違背事件進(jìn)行分類描述。提出基于ATG-CPN模型的狀態(tài)空間搜索方法，生成到達(dá)攻擊狀態(tài)的攻擊序列，減少了狀態(tài)空間中搜索的狀態(tài)數(shù)，避免生成虛假攻擊。同時(shí)提出基于ATGx-CPN模型的on-the-fly攻擊序列生成方法，該方法不需要對(duì)整個(gè)狀態(tài)空間進(jìn)行廣度或深度搜索，基于部分狀態(tài)空間生成有效的攻擊序列。
　　(3)提出一種基于攻擊