安全協(xié)議是實(shí)現(xiàn)安全的分布式系統(tǒng)的基礎(chǔ),所以保證其正確地工作至關(guān)重要。不幸的是,安全協(xié)議的設(shè)計(jì)存在一些非常微妙的細(xì)節(jié),很難保證在設(shè)計(jì)過(guò)程中就能發(fā)現(xiàn)可能存在的漏洞。為此,在過(guò)去的20年間,研究人員提出了許多嚴(yán)格的形式化分析方法用于協(xié)議的安全性分析。其中,一種名為“BAN邏輯”的基于邏輯推理的分析方法,因其以通俗的概念來(lái)偵測(cè)協(xié)議中存在的漏洞和冗余,而獲得了廣泛的應(yīng)用和好評(píng)。GNY是BAN的眾多后繼者中的一員,它擴(kuò)展了BAN邏輯中的許多內(nèi)容使得便于利用GNY開(kāi)發(fā)自動(dòng)化驗(yàn)證系統(tǒng)。 基于形式邏輯的思想,一種名為“信任多集”的形式化分析方法被提出來(lái),它明確指明了保證密碼協(xié)議足夠安全的充分必要條件,同時(shí)對(duì)于存在安全性缺失的密碼協(xié)議,能夠有限度地給出構(gòu)造攻擊的結(jié)構(gòu)。本文將闡述,信任多集在經(jīng)過(guò)改進(jìn)和完善后,不僅可用于手工分析也便于開(kāi)發(fā)自動(dòng)驗(yàn)證系統(tǒng)。 BMF Package就是基于“信任多集”所開(kāi)發(fā)出的一套自動(dòng)化驗(yàn)證系統(tǒng)。它由Prolog語(yǔ)言編寫(xiě)的分析器BMF Analyzer和可視化建模工具Visual BMF組成。它借鑒了南非開(kāi)普敦大學(xué)基于GNY邏輯所開(kāi)發(fā)的Spear2系統(tǒng)。 本文的結(jié)構(gòu)如下：第2章主要...

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

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

【文章目錄】：
摘要
Abstract
目錄
圖目錄
表目錄
第一章 緒論
    1.1 背景及其意義
    1.2 我的工作
    1.3 論文的組織結(jié)構(gòu)
第二章 安全協(xié)議的介紹
    2.1 安全協(xié)議形式化
    2.2 安全協(xié)議的安全性質(zhì)
    2.3 安全協(xié)議的分類(lèi)
    2.4 安全協(xié)議的漏洞以及可能攻擊
    2.5 本章小結(jié)
第三章 安全協(xié)議形式化分析的研究與進(jìn)展
    3.1 形式邏輯分析方法
    3.2 模型檢測(cè)方法
    3.3 定理證明方法
    3.4 本章小結(jié)
第四章 BAN邏輯的介紹
    4.1 BAN邏輯的前提假設(shè)和適用范圍
    4.2 基本概念和符號(hào)
    4.3 基本推導(dǎo)規(guī)則
    4.4 安全協(xié)議的理想化
    4.5 BAN邏輯的推導(dǎo)過(guò)程
    4.6 BAN邏輯中的認(rèn)證協(xié)議的目標(biāo)
    4.7 使用BAN邏輯進(jìn)行協(xié)議分析
    4.8 BAN邏輯的缺陷
第五章 信任多集形式化分析方法的改進(jìn)
    5.1 一些引論
    5.2 擁有和關(guān)聯(lián)
    5.3 基本概念和符號(hào)
    5.4 基本推導(dǎo)規(guī)則
    5.5 安全協(xié)議的形式化
    5.6 信任多集中的初始化假設(shè)
    5.7 信任多集的計(jì)算模型
    5.8 信任多集的推導(dǎo)過(guò)程
    5.9 信任多集中的安全協(xié)議目標(biāo)
    5.10 使用信任多集進(jìn)行協(xié)議分析
    5.11 本章小結(jié)
第六章 信任多集自動(dòng)化分析的實(shí)現(xiàn)
    6.1 Spear2的簡(jiǎn)單介紹
    6.2 Prolog的簡(jiǎn)單介紹
    6.3 信任多集的Prolog表示
    6.4 一些預(yù)備知識(shí)
    6.5 前向鏈推導(dǎo)引擎的實(shí)現(xiàn)
    6.6 ^*(M)集合的實(shí)現(xiàn)
    6.7 推導(dǎo)規(guī)則的實(shí)現(xiàn)
    6.8 使用Prolog輸出推導(dǎo)過(guò)程
    6.9 可視化定制環(huán)境-Visual BMF
    6.10 使用BMF Package對(duì)Otway-Rees協(xié)議進(jìn)行分析
    6.11 本章小結(jié)
第七章 結(jié)束語(yǔ)
    7.1 總結(jié)
    7.2 展望
參考文獻(xiàn)
致謝



本文編號(hào)：3735226