掃一掃
關(guān)注中圖網(wǎng)
官方微博
安全協(xié)議形式化分析與驗(yàn)證 版權(quán)信息
- ISBN：9787030626332
- 條形碼：9787030626332 ; 978-7-03-062633-2
- 裝幀：平裝-膠訂
- 冊數(shù)：暫無
- 重量：暫無
- 所屬分類：>
安全協(xié)議形式化分析與驗(yàn)證 本書特色
本書內(nèi)容主要包括以下部分：安全協(xié)議形式化分析背景及研究現(xiàn)狀。介紹了安全協(xié)議及形式化方法基本概念，安全協(xié)議形式化分析研究發(fā)展歷史和國內(nèi)外研究現(xiàn)狀。形式化方法基本理論。對模態(tài)邏輯、模型檢測，定理證明三類形式化方法進(jìn)行了詳細(xì)闡述和對比分析，介紹了Murφ和Spin具有代表性的形式化分析工具。安全協(xié)議。介紹了安全協(xié)議的基本概念及分類，從安全協(xié)議受攻擊類型角度提出安全協(xié)議形式化分析的必要性。
安全協(xié)議形式化分析與驗(yàn)證 內(nèi)容簡介
《安全協(xié)議形式化分析與驗(yàn)證》是作者多年從事安全協(xié)議形式化分析與驗(yàn)證相關(guān)科研工作的總結(jié)，主要對兩種形式化方法做了歸納：基于SPIN工具的模型檢測和事件邏輯。 《安全協(xié)議形式化分析與驗(yàn)證》主要內(nèi)容如下：介紹了安全協(xié)議形式化分析的研究現(xiàn)狀、主要技術(shù)流派，以及協(xié)議描述語言ProDL，闡述了基于算法知識邏輯的網(wǎng)絡(luò)安全協(xié)議模型檢測分析方法，用于顯式地刻畫入侵者模型能力；在網(wǎng)絡(luò)安全協(xié)議驗(yàn)證模型生成系統(tǒng)中，采用偏序歸約、語法重定序以及靜態(tài)分析等優(yōu)化策略，有效緩解模型檢測過程中狀態(tài)爆炸問題；對事件邏輯進(jìn)行擴(kuò)展，提出一系列規(guī)則，對安全協(xié)議進(jìn)行形式化描述，無需顯性刻畫入侵者模型，只需分析協(xié)議動作之間的匹配順序關(guān)系即可對協(xié)議的安全性進(jìn)行證明。
安全協(xié)議形式化分析與驗(yàn)證 目錄
目錄
前言
第1章 緒論 1
1.1 安全協(xié)議形式化分析背景 1
1.2 安全協(xié)議形式化分析研究現(xiàn)狀 3
參考文獻(xiàn) 6
第2章 形式化方法基本理論 10
2.1 形式化方法概述 10
2.2 模態(tài)邏輯 11
2.2.1 BAN邏輯 11
2.2.2 BAN類邏輯 14
2.2.3 Kailar邏輯 15
2.3 模型檢測 15
2.3.1 FDR 16
2.3.2 NRL協(xié)議分析器 19
2.3.3 Murφ 21
2.3.4 SPIN 23
2.4 定理證明 26
2.4.1 Paulson歸納法 27
2.4.2 串空間模型 28
2.4.3 Spi演算證明方法 29
2.4.4 PCL證明方法 30
2.4.5 事件邏輯證明方法 33
2.5 比較與分析 35
參考文獻(xiàn) 36
第3章 安全協(xié)議 39
3.1 安全協(xié)議概念 39
3.2 安全協(xié)議分類 40
3.2.1 ISO/IEC 11770-2密鑰建立機(jī)制6協(xié)議 40
3.2.2 NSSK協(xié)議 41
3.2.3 Kerberos認(rèn)證協(xié)議 42
3.2.4 ISO/IEC 9798-3協(xié)議 44
3.2.5 NSPK協(xié)議 44
3.3 協(xié)議安全屬性 45
3.4 協(xié)議安全構(gòu)建方法 46
3.4.1 Hash函數(shù) 48
3.4.2 隨機(jī)數(shù) 49
3.4.3 時(shí)間戳 50
3.5 協(xié)議攻擊者模型及其攻擊類型 51
3.5.1 Dolev-Yao攻擊者模型 52
3.5.2 攻擊類型 53
參考文獻(xiàn) 53
第4章 基于模型檢測的安全協(xié)議分析 55
4.1 安全協(xié)議形式化表示 55
4.1.1 原子消息(基本約定) 55
4.1.2 消息 55
4.1.3 動作 56
4.1.4 協(xié)議 57
4.1.5 跡 57
4.2 消息生成規(guī)則 58
4.3 基于算法知識邏輯的協(xié)議形式化分析 61
4.3.1 多智體系統(tǒng) 62
4.3.2 算法知識邏輯 62
4.3.3 算法知識邏輯分析協(xié)議 64
4.4 時(shí)態(tài)邏輯 69
4.4.1 Kripke結(jié)構(gòu) 70
4.4.2 CTL*、CTL和LTL 70
4.4.3 并發(fā)系統(tǒng)性質(zhì)描述 72
4.4.4 實(shí)例 73
4.5 形式化分析流程 74
4.5.1 形式化建模 75
4.5.2 協(xié)議安全性質(zhì)刻畫 79
4.5.3 形式化驗(yàn)證 79
4.6 驗(yàn)證模型優(yōu)化策略 79
4.6.1 靜態(tài)分析 79
4.6.2 語法重定序 84
4.6.3 偏序歸約 84
4.6.4 優(yōu)化策略對比 87
4.7 與其他方法對比 88
4.7.1 與認(rèn)證邏輯對比 89
4.7.2 與FDR對比 91
4.7.3 與Murφ對比 93
4.7.4 與NRL協(xié)議分析器對比 95
4.7.5 與Athena對比 97
4.7.6 與Isabelle對比 100
4.7.7 與BRUTUS對比 101
參考文獻(xiàn) 103
第5章 網(wǎng)絡(luò)安全協(xié)議驗(yàn)證模型生成系統(tǒng) 108
5.1 系統(tǒng)概述 108
5.1.1 系統(tǒng)簡介 108
5.1.2 系統(tǒng)功能 110
5.2 系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn) 112
5.2.1 整體設(shè)計(jì) 112
5.2.2 模塊設(shè)計(jì) 112
5.2.3 協(xié)議描述語言ProDL 124
5.2.4 Needham-Schroeder公開密鑰協(xié)議分析與驗(yàn)證 130
5.2.5 BAN-Yahalom三方對稱密鑰認(rèn)證協(xié)議分析與驗(yàn)證 132
5.2.6 CMP1可信第三方電子商務(wù)協(xié)議分析與驗(yàn)證 133
參考文獻(xiàn) 135
第6章 基于事件邏輯的安全協(xié)議形式化分析 137
6.1 事件系統(tǒng) 137
6.1.1 符號說明 137
6.1.2 消息自動機(jī) 138
6.1.3 語法語義 139
6.1.4 不可猜測的原子 140
6.1.5 事件結(jié)構(gòu) 140
6.1.6 事件類 142
6.2 事件邏輯公理、推論及性質(zhì) 143
6.2.1 事件邏輯公理 143
6.2.2 事件邏輯推論及性質(zhì) 146
6.3 事件邏輯形式化描述協(xié)議 147
6.4 基于事件邏輯的安全協(xié)議證明 150
6.4.1 推理規(guī)則 150
6.4.2 兩方安全協(xié)議證明流程 151
6.4.3 三方安全協(xié)議證明流程 153
6.5 與其他典型證明方法對比 154
6.5.1 PCL 154
6.5.2 BAN類邏輯 155
6.5.3 串空間理論 155
參考文獻(xiàn) 156
第7章 總結(jié)與展望 158
7.1 研究成果總結(jié) 158
7.2 下一步研究工作 159
前言
第1章 緒論 1
1.1 安全協(xié)議形式化分析背景 1
1.2 安全協(xié)議形式化分析研究現(xiàn)狀 3
參考文獻(xiàn) 6
第2章 形式化方法基本理論 10
2.1 形式化方法概述 10
2.2 模態(tài)邏輯 11
2.2.1 BAN邏輯 11
2.2.2 BAN類邏輯 14
2.2.3 Kailar邏輯 15
2.3 模型檢測 15
2.3.1 FDR 16
2.3.2 NRL協(xié)議分析器 19
2.3.3 Murφ 21
2.3.4 SPIN 23
2.4 定理證明 26
2.4.1 Paulson歸納法 27
2.4.2 串空間模型 28
2.4.3 Spi演算證明方法 29
2.4.4 PCL證明方法 30
2.4.5 事件邏輯證明方法 33
2.5 比較與分析 35
參考文獻(xiàn) 36
第3章 安全協(xié)議 39
3.1 安全協(xié)議概念 39
3.2 安全協(xié)議分類 40
3.2.1 ISO/IEC 11770-2密鑰建立機(jī)制6協(xié)議 40
3.2.2 NSSK協(xié)議 41
3.2.3 Kerberos認(rèn)證協(xié)議 42
3.2.4 ISO/IEC 9798-3協(xié)議 44
3.2.5 NSPK協(xié)議 44
3.3 協(xié)議安全屬性 45
3.4 協(xié)議安全構(gòu)建方法 46
3.4.1 Hash函數(shù) 48
3.4.2 隨機(jī)數(shù) 49
3.4.3 時(shí)間戳 50
3.5 協(xié)議攻擊者模型及其攻擊類型 51
3.5.1 Dolev-Yao攻擊者模型 52
3.5.2 攻擊類型 53
參考文獻(xiàn) 53
第4章 基于模型檢測的安全協(xié)議分析 55
4.1 安全協(xié)議形式化表示 55
4.1.1 原子消息(基本約定) 55
4.1.2 消息 55
4.1.3 動作 56
4.1.4 協(xié)議 57
4.1.5 跡 57
4.2 消息生成規(guī)則 58
4.3 基于算法知識邏輯的協(xié)議形式化分析 61
4.3.1 多智體系統(tǒng) 62
4.3.2 算法知識邏輯 62
4.3.3 算法知識邏輯分析協(xié)議 64
4.4 時(shí)態(tài)邏輯 69
4.4.1 Kripke結(jié)構(gòu) 70
4.4.2 CTL*、CTL和LTL 70
4.4.3 并發(fā)系統(tǒng)性質(zhì)描述 72
4.4.4 實(shí)例 73
4.5 形式化分析流程 74
4.5.1 形式化建模 75
4.5.2 協(xié)議安全性質(zhì)刻畫 79
4.5.3 形式化驗(yàn)證 79
4.6 驗(yàn)證模型優(yōu)化策略 79
4.6.1 靜態(tài)分析 79
4.6.2 語法重定序 84
4.6.3 偏序歸約 84
4.6.4 優(yōu)化策略對比 87
4.7 與其他方法對比 88
4.7.1 與認(rèn)證邏輯對比 89
4.7.2 與FDR對比 91
4.7.3 與Murφ對比 93
4.7.4 與NRL協(xié)議分析器對比 95
4.7.5 與Athena對比 97
4.7.6 與Isabelle對比 100
4.7.7 與BRUTUS對比 101
參考文獻(xiàn) 103
第5章 網(wǎng)絡(luò)安全協(xié)議驗(yàn)證模型生成系統(tǒng) 108
5.1 系統(tǒng)概述 108
5.1.1 系統(tǒng)簡介 108
5.1.2 系統(tǒng)功能 110
5.2 系統(tǒng)設(shè)計(jì)與實(shí)現(xiàn) 112
5.2.1 整體設(shè)計(jì) 112
5.2.2 模塊設(shè)計(jì) 112
5.2.3 協(xié)議描述語言ProDL 124
5.2.4 Needham-Schroeder公開密鑰協(xié)議分析與驗(yàn)證 130
5.2.5 BAN-Yahalom三方對稱密鑰認(rèn)證協(xié)議分析與驗(yàn)證 132
5.2.6 CMP1可信第三方電子商務(wù)協(xié)議分析與驗(yàn)證 133
參考文獻(xiàn) 135
第6章 基于事件邏輯的安全協(xié)議形式化分析 137
6.1 事件系統(tǒng) 137
6.1.1 符號說明 137
6.1.2 消息自動機(jī) 138
6.1.3 語法語義 139
6.1.4 不可猜測的原子 140
6.1.5 事件結(jié)構(gòu) 140
6.1.6 事件類 142
6.2 事件邏輯公理、推論及性質(zhì) 143
6.2.1 事件邏輯公理 143
6.2.2 事件邏輯推論及性質(zhì) 146
6.3 事件邏輯形式化描述協(xié)議 147
6.4 基于事件邏輯的安全協(xié)議證明 150
6.4.1 推理規(guī)則 150
6.4.2 兩方安全協(xié)議證明流程 151
6.4.3 三方安全協(xié)議證明流程 153
6.5 與其他典型證明方法對比 154
6.5.1 PCL 154
6.5.2 BAN類邏輯 155
6.5.3 串空間理論 155
參考文獻(xiàn) 156
第7章 總結(jié)與展望 158
7.1 研究成果總結(jié) 158
7.2 下一步研究工作 159
展開全部
書友推薦
- >
新文學(xué)天穹兩巨星--魯迅與胡適/紅燭學(xué)術(shù)叢書(紅燭學(xué)術(shù)叢書)
- >
羅曼·羅蘭讀書隨筆-精裝
- >
伊索寓言-世界文學(xué)名著典藏-全譯本
- >
巴金－再思錄
- >
企鵝口袋書系列·偉大的思想20:論自然選擇(英漢雙語)
- >
自卑與超越
- >
經(jīng)典常談
- >
名家?guī)阕x魯迅:朝花夕拾
本類暢銷
