安全協(xié)議是以密碼學(xué)為基礎(chǔ)的協(xié)議,它在因特網(wǎng)和分布式系統(tǒng)中提供各種各樣的安全服務(wù)。近年來(lái),利用形式化方法分析安全協(xié)議正在成為一個(gè)新的趨勢(shì)。本文首先在分布式時(shí)序邏輯的基礎(chǔ)上,給出了這個(gè)邏輯中局部公式的幾組等價(jià)性定理并進(jìn)行了證明,并和時(shí)序邏輯中的等價(jià)性公理進(jìn)行了比較。然后用分布式時(shí)序邏輯描述了IEEE802.11i協(xié)議,給出了這個(gè)協(xié)議的事件結(jié)構(gòu)模型,證明了三個(gè)主體之間的相互認(rèn)證性。其次在分布式時(shí)序邏輯的基礎(chǔ)上,增加了存在量詞和全稱量詞,提出了分布式計(jì)算樹(shù)時(shí)序邏輯。給出了分布式計(jì)算樹(shù)時(shí)序邏輯的狀態(tài)公式和路徑公式的定義,以及這個(gè)邏輯的語(yǔ)義。同時(shí)也給出了分布式計(jì)算樹(shù)時(shí)序邏輯中局部狀態(tài)公式的幾組等價(jià)性定理,并進(jìn)行了證明。最后利用本文提出的分布式計(jì)算樹(shù)時(shí)序邏輯描述了多方認(rèn)證電子郵件協(xié)議,給出了這個(gè)協(xié)議的事件結(jié)構(gòu)模型以及一些公平性公理。在有可信第三方參與和沒(méi)有可信第三方參與的兩種情況下,證明了發(fā)送者的不可否認(rèn)性和接收者的不可否認(rèn)性。 

【文章來(lái)源】：南京航空航天大學(xué)江蘇省 211工程院校

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

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

【文章目錄】：
摘要
ABSTRACT
第一章 緒論
    1.1 安全協(xié)議
    1.2 安全協(xié)議的形式化方法
    1.3 時(shí)序邏輯和分布式時(shí)序邏輯
    1.4 本文的研究?jī)?nèi)容及結(jié)構(gòu)安排
第二章 分布式時(shí)序邏輯
    2.1 DTL 的語(yǔ)形
    2.2 DTL 的語(yǔ)義
    2.3 DTL 中公式的等價(jià)性定理
        2.3.1 對(duì)偶律
        2.3.2 冪等律
        2.3.3 吸收律
        2.3.4 分配律
        2.3.5 擴(kuò)張律
    2.4 本章小結(jié)
第三章 用分布式時(shí)序邏輯驗(yàn)證IEEE802.11i 協(xié)議
    3.1 IEEE802.11i 協(xié)議
    3.2 IEEE802.11i 協(xié)議的DTL 模型
        3.2.1 消息以及和消息有關(guān)的概念
        3.2.2 基于信道的模型
        3.2.3 DTL 的公理
            3.2.3.1 K 公理以及由K 公理推出的公理
            3.2.3.2 新鮮性和唯一性公理
            3.2.3.3 關(guān)于信道CH 和主體的公理
            3.2.3.4 關(guān)于公鑰、私鑰和共享密鑰的公理
        3.2.4 引理及命題
    3.3 IEEE802.11i 協(xié)議的網(wǎng)絡(luò)模型和事件結(jié)構(gòu)模型
    3.4 IEEE802.11i 協(xié)議的認(rèn)證性
        3.4.1 申請(qǐng)者認(rèn)證
        3.4.2 認(rèn)證者認(rèn)證
        3.4.3 認(rèn)證服務(wù)器認(rèn)證
    3.5 本章小結(jié)
第四章 分布式計(jì)算樹(shù)時(shí)序邏輯
    4.1 DCTL 的語(yǔ)形
    4.2 DCTL 的語(yǔ)義
    4.3 DCTL 中公式的等價(jià)性定理
        4.3.1 對(duì)偶律
        4.3.2 分配律
        4.3.3 擴(kuò)張律
    4.4 本章小節(jié)
第五章 用分布式計(jì)算樹(shù)時(shí)序邏輯分析多方認(rèn)證電子郵件協(xié)議
    5.1 多方認(rèn)證電子郵件協(xié)議
    5.2 多方認(rèn)證電子郵件協(xié)議的網(wǎng)絡(luò)模型
        5.2.1 沒(méi)有可信第三方的參與
        5.2.2 有可信第三方的參與
    5.3 用 DCTL 描述多方認(rèn)證電子郵件協(xié)議
        5.3.1 交換子協(xié)議的事件結(jié)構(gòu)模型
        5.3.2 取消子協(xié)議的事件結(jié)構(gòu)模型
        5.3.3 結(jié)束子協(xié)議的事件結(jié)構(gòu)模型
    5.4 多方認(rèn)證電子郵件協(xié)議的不可否認(rèn)性
        5.4.1 發(fā)起者的不可否認(rèn)性
            5.4.1.1 沒(méi)有可信第三方的參與
            5.4.1.2 有可信第三方的參與
        5.4.2 接收者的不可否認(rèn)性
            5.4.2.1 沒(méi)有可信第三方的參與
            5.4.2.2 有可信第三方的參與
    5.5 本章小結(jié)
第六章 總結(jié)與展望
    6.1 總結(jié)
    6.2 展望
參考文獻(xiàn)
致謝
在學(xué)期間研究成果及發(fā)表的學(xué)術(shù)論文
附錄


【參考文獻(xiàn)】：
期刊論文
[1]802.11i認(rèn)證協(xié)議可驗(yàn)安全性形式化分析[J]. 宋宇波,胡愛(ài)群,姚冰心.  中國(guó)工程科學(xué). 2010(01)
[2]Yahalom協(xié)議的分析及改進(jìn)方案[J]. 陳春玲,趙艷春.  計(jì)算機(jī)應(yīng)用與軟件. 2008(07)
[3]IEEE 802.11i協(xié)議的形式化分析[J]. 吳開(kāi)貴,徐成,廖振嵐.  計(jì)算機(jī)應(yīng)用. 2008(05)
[4]IEEE802.11i中四次握手過(guò)程的安全分析和改進(jìn)[J]. 梁峰,史杏榮,曲阜平.  計(jì)算機(jī)工程. 2007(03)
[5]基于簽密的多方認(rèn)證郵件協(xié)議[J]. 王彩芬,賈愛(ài)庫(kù),劉軍龍,于成尊.  電子學(xué)報(bào). 2005(11)
[6]公平的多方不可否認(rèn)協(xié)議[J]. 何冰,李肖堅(jiān),夏春和,夏克儉.  計(jì)算機(jī)工程與應(yīng)用. 2005(27)
[7]電子商務(wù)協(xié)議中的可信第三方角色[J]. 卿斯?jié)h.  軟件學(xué)報(bào). 2003(11)
[8]安全協(xié)議20年研究進(jìn)展[J]. 卿斯?jié)h.  軟件學(xué)報(bào). 2003(10)
[9]安全協(xié)議的設(shè)計(jì)與邏輯分析[J]. 卿斯?jié)h.  軟件學(xué)報(bào). 2003(07)
[10]安全協(xié)議的形式化需求及驗(yàn)證[J]. 劉怡文,李偉琴.  計(jì)算機(jī)工程與應(yīng)用. 2002(17)



本文編號(hào)：3138982