發(fā)布時(shí)間：2021-11-12 12:41

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

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

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

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

【文章目錄】：
摘要
ABSTRACT
縮略詞
第一章 引言
    1.1 研究背景及意義
    1.2 論文的貢獻(xiàn)
    1.3 論文的組織
第二章 相關(guān)研究概述
    2.1 安全協(xié)議及其性質(zhì)
        2.1.1 安全協(xié)議分類(lèi)
        2.1.2 安全屬性
    2.2 形式化建模方法
    2.3 安全協(xié)議形式化分析方法
        2.3.1 基于推理證明的模態(tài)邏輯方法
        2.3.2 定理證明方法
        2.3.3 基于類(lèi)型檢測(cè)的方法
        2.3.4 模型檢測(cè)方法
    2.4 攻擊者模型
        2.4.1 Dolev-Yao攻擊者模型
        2.4.2 安全協(xié)議的攻擊分類(lèi)
    2.5 攻擊序列生成方法
        2.5.1 基于定理證明的攻擊序列生成方法
        2.5.2 基于模型檢測(cè)的攻擊序列生成方法
    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 本文研究的問(wèn)題
    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 攻擊策略的評(píng)判
    5.3 攻擊目的AP-CPN形式化描述
    5.4 基于攻擊目的的攻擊序列選擇方法
    5.5 實(shí)例分析：TMN協(xié)議系統(tǒng)
        5.5.1 TMN協(xié)議的攻擊策略評(píng)判
        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ā)展趨勢(shì)[J]. 薛銳,雷新鋒.  中國(guó)科學(xué)院院刊. 2011(03)
[2]基于面向?qū)ο髸r(shí)間Petri網(wǎng)的密碼協(xié)議分析[J]. 劉雪艷,吳慧欣,張強(qiáng),王彩芬.  計(jì)算機(jī)工程. 2009(13)
[3]安全協(xié)議的形式化分析技術(shù)與方法[J]. 薛銳,馮登國(guó).  計(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]. 李夢(mèng)君,李舟軍,陳火旺.  計(jì)算機(jī)研究與發(fā)展. 2004(07)
[6]安全協(xié)議形式化分析理論與方法研究綜述[J]. 馮登國(guó),范紅.  中國(guó)科學(xué)院研究生院學(xué)報(bào). 2003(04)
[7]一種通信協(xié)議測(cè)試序列生成的新方法[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