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

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

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

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

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

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