隨著計(jì)算機(jī)網(wǎng)絡(luò)的迅速發(fā)展,信息通信的安全問題變得越來越突出,越來越復(fù)雜,解決安全問題對許多網(wǎng)絡(luò)應(yīng)用來說具有重要意義。目前,網(wǎng)絡(luò)通信安全問題的解決方案中,安全協(xié)議是最有效的手段之一。由于網(wǎng)絡(luò)本身的開放性,使得網(wǎng)絡(luò)中存在著各種安全威脅,攻擊者可以采用多種方式對安全協(xié)議進(jìn)行攻擊,破壞其安全屬性。分析安全協(xié)議中可能存在的缺陷很難完全由人工來識(shí)別,因此,需要借助形式化的分析方法和工具來完成。安全協(xié)議的形式化分析過程包含安全協(xié)議系統(tǒng)建模、安全屬性驗(yàn)證、以及攻擊序列生成等。本文通過分析安全協(xié)議模型中攻擊者的“任意”性行為和協(xié)議的多次并發(fā)會(huì)話問題,提出了一種改進(jìn)的攻擊者模型和多并發(fā)會(huì)話劃分分析方法。針對安全屬性驗(yàn)證和攻擊序列生成問題,采用安全屬性違背事件對不安全狀態(tài)進(jìn)行分類描述,提出基于安全屬性違背事件生成攻擊序列的兩種方法：狀態(tài)空間搜索法和on-the-fly生成方法�；诎踩珜傩赃`背事件生成攻擊序列的方法能夠有效地控制搜索范圍,提高搜索效率。最后通過分析安全協(xié)議中的數(shù)據(jù)特征,提取能夠構(gòu)成攻擊的攻擊策略,并依據(jù)攻擊策略確定攻擊目的,構(gòu)建基于攻擊目的的模型,選擇生成攻擊序列,有效地削減安全協(xié)議模型檢測... 

【文章來源】：內(nèi)蒙古大學(xué)內(nèi)蒙古自治區(qū) 211工程院校

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

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

【文章目錄】：
摘要
ABSTRACT
縮略詞
第一章 引言
    1.1 研究背景及意義
    1.2 論文的貢獻(xiàn)
    1.3 論文的組織
第二章 相關(guān)研究概述
    2.1 安全協(xié)議及其性質(zhì)
        2.1.1 安全協(xié)議分類
        2.1.2 安全屬性
    2.2 形式化建模方法
    2.3 安全協(xié)議形式化分析方法
        2.3.1 基于推理證明的模態(tài)邏輯方法
        2.3.2 定理證明方法
        2.3.3 基于類型檢測的方法
        2.3.4 模型檢測方法
    2.4 攻擊者模型
        2.4.1 Dolev-Yao攻擊者模型
        2.4.2 安全協(xié)議的攻擊分類
    2.5 攻擊序列生成方法
        2.5.1 基于定理證明的攻擊序列生成方法
        2.5.2 基于模型檢測的攻擊序列生成方法
    2.6 基于CP-nets模型的形式化方法
        2.6.1 CP-nets模型形式化定義
        2.6.2 CP-nets的主要分析技術(shù)
        2.6.3 CP-nets應(yīng)用現(xiàn)狀
    2.7 本文研究的問題
    2.8 本章小結(jié)
第三章 安全協(xié)議的形式化建模
    3.1 方法概述
    3.2 安全協(xié)議建模約束
    3.3 Dolev-Yao攻擊者模型的改進(jìn)
        3.3.1 Dolev-Yao攻擊者模型
        3.3.2 一種改進(jìn)的攻擊者模型
        3.3.3 應(yīng)用實(shí)例：NS協(xié)議
    3.4 多并發(fā)會(huì)話劃分分析方法
    3.5 并發(fā)行為控制
    3.6 實(shí)例系統(tǒng)：TMN協(xié)議
        3.6.1 建模約束條件
        3.6.2 TMN協(xié)議的數(shù)據(jù)建模
        3.6.3 TMN協(xié)議的CP-nets建模
        3.6.4 TMN協(xié)議的CP-nets模型安全屬性驗(yàn)證分析
    3.7 小結(jié)
第四章 基于CP-nets的安全協(xié)議模型驗(yàn)證與攻擊序列生成
    4.1 方法概述
    4.2 ATG-CPN模型形式化定義
    4.3 安全屬性描述
        4.3.1 保密性屬性形式化定義
        4.3.2 認(rèn)證性屬性形式化定義
    4.4 基于安全屬性違背事件的攻擊序列生成算法—狀態(tài)空間搜索法
        4.4.1 安全屬性違背事件
        4.4.2 算法的形式描述
        4.4.3 NS協(xié)議的攻擊序列生成
    4.5 On-the-fly安全協(xié)議攻擊序列生成
        4.5.1 ATG_X-CPN模型描述
        4.5.2 On-the-fly攻擊序列生成方法
    4.6 實(shí)例分析：TMN協(xié)議系統(tǒng)
        4.6.1 TMN協(xié)議的ATG-CPN模型
        4.6.2 基于狀態(tài)空間搜索方法的攻擊序列生成與分析
    4.7 本章小結(jié)
第五章 基于攻擊目的的攻擊序列選擇
    5.1 方法概述
    5.2 安全協(xié)議的主要攻擊方式
        5.2.1 攻擊者的攻擊策略和攻擊行為
        5.2.2 攻擊策略的評判
    5.3 攻擊目的AP-CPN形式化描述
    5.4 基于攻擊目的的攻擊序列選擇方法
    5.5 實(shí)例分析：TMN協(xié)議系統(tǒng)
        5.5.1 TMN協(xié)議的攻擊策略評判
        5.5.2 TMN協(xié)議的攻擊策略建模
        5.5.3 TMN協(xié)議的攻擊序列選擇生成
    5.6 本章小結(jié)
第六章 結(jié)論及進(jìn)一步工作
    6.1 論文的主要結(jié)論
    6.2 進(jìn)一步的研究工作
參考文獻(xiàn)
致謝
攻讀博士學(xué)位期間發(fā)表論文
攻讀博士學(xué)位期間主持和參加的科研項(xiàng)目


【參考文獻(xiàn)】：
期刊論文
[1]安全協(xié)議:信息安全保障的靈魂——安全協(xié)議分析研究現(xiàn)狀與發(fā)展趨勢[J]. 薛銳,雷新鋒.  中國科學(xué)院院刊. 2011(03)
[2]基于面向?qū)ο髸r(shí)間Petri網(wǎng)的密碼協(xié)議分析[J]. 劉雪艷,吳慧欣,張強(qiáng),王彩芬.  計(jì)算機(jī)工程. 2009(13)
[3]安全協(xié)議的形式化分析技術(shù)與方法[J]. 薛銳,馮登國.  計(jì)算機(jī)學(xué)報(bào). 2006(01)
[4]串空間代數(shù)缺陷到實(shí)際攻擊的轉(zhuǎn)換[J]. 沈海峰,黃河燕,陳肇雄.  計(jì)算機(jī)科學(xué). 2005(07)
[5]基于進(jìn)程代數(shù)安全協(xié)議驗(yàn)證的研究綜述[J]. 李夢君,李舟軍,陳火旺.  計(jì)算機(jī)研究與發(fā)展. 2004(07)
[6]安全協(xié)議形式化分析理論與方法研究綜述[J]. 馮登國,范紅.  中國科學(xué)院研究生院學(xué)報(bào). 2003(04)
[7]一種通信協(xié)議測試序列生成的新方法[J]. 孫宇霖,屈玉貴,趙保華.  通信學(xué)報(bào). 2001(06)
[8]隨機(jī)Petri網(wǎng)的分解和壓縮技術(shù)[J]. 林闖.  軟件學(xué)報(bào). 1997(07)

碩士論文
[1]安全協(xié)議攻擊序列重構(gòu)技術(shù)研究[D]. 張超.解放軍信息工程大學(xué) 2008



本文編號(hào)：3490934