掃一掃
關注中圖網
官方微博
本類五星書更多>
-
>
全國計算機等級考試最新真考題庫模擬考場及詳解·二級MSOffice高級應用
-
>
決戰行測5000題(言語理解與表達)
-
>
軟件性能測試.分析與調優實踐之路
-
>
第一行代碼Android
-
>
JAVA持續交付
-
>
EXCEL最強教科書(完全版)(全彩印刷)
-
>
深度學習
安全協議形式化分析與驗證 版權信息
- ISBN：9787030626332
- 條形碼：9787030626332 ; 978-7-03-062633-2
- 裝幀：平裝-膠訂
- 冊數：暫無
- 重量：暫無
- 所屬分類：>
安全協議形式化分析與驗證 本書特色
本書內容主要包括以下部分：安全協議形式化分析背景及研究現狀。介紹了安全協議及形式化方法基本概念，安全協議形式化分析研究發展歷史和國內外研究現狀。形式化方法基本理論。對模態邏輯、模型檢測，定理證明三類形式化方法進行了詳細闡述和對比分析，介紹了Murφ和Spin具有代表性的形式化分析工具。安全協議。介紹了安全協議的基本概念及分類，從安全協議受攻擊類型角度提出安全協議形式化分析的必要性。
安全協議形式化分析與驗證 內容簡介
《安全協議形式化分析與驗證》是作者多年從事安全協議形式化分析與驗證相關科研工作的總結，主要對兩種形式化方法做了歸納：基于SPIN工具的模型檢測和事件邏輯。 《安全協議形式化分析與驗證》主要內容如下：介紹了安全協議形式化分析的研究現狀、主要技術流派，以及協議描述語言ProDL，闡述了基于算法知識邏輯的網絡安全協議模型檢測分析方法，用于顯式地刻畫入侵者模型能力；在網絡安全協議驗證模型生成系統中，采用偏序歸約、語法重定序以及靜態分析等優化策略，有效緩解模型檢測過程中狀態爆炸問題；對事件邏輯進行擴展，提出一系列規則，對安全協議進行形式化描述，無需顯性刻畫入侵者模型，只需分析協議動作之間的匹配順序關系即可對協議的安全性進行證明。
安全協議形式化分析與驗證 目錄
目錄
前言
第1章 緒論 1
1.1 安全協議形式化分析背景 1
1.2 安全協議形式化分析研究現狀 3
參考文獻 6
第2章 形式化方法基本理論 10
2.1 形式化方法概述 10
2.2 模態邏輯 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協議分析器 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
參考文獻 36
第3章 安全協議 39
3.1 安全協議概念 39
3.2 安全協議分類 40
3.2.1 ISO/IEC 11770-2密鑰建立機制6協議 40
3.2.2 NSSK協議 41
3.2.3 Kerberos認證協議 42
3.2.4 ISO/IEC 9798-3協議 44
3.2.5 NSPK協議 44
3.3 協議安全屬性 45
3.4 協議安全構建方法 46
3.4.1 Hash函數 48
3.4.2 隨機數 49
3.4.3 時間戳 50
3.5 協議攻擊者模型及其攻擊類型 51
3.5.1 Dolev-Yao攻擊者模型 52
3.5.2 攻擊類型 53
參考文獻 53
第4章 基于模型檢測的安全協議分析 55
4.1 安全協議形式化表示 55
4.1.1 原子消息(基本約定) 55
4.1.2 消息 55
4.1.3 動作 56
4.1.4 協議 57
4.1.5 跡 57
4.2 消息生成規則 58
4.3 基于算法知識邏輯的協議形式化分析 61
4.3.1 多智體系統 62
4.3.2 算法知識邏輯 62
4.3.3 算法知識邏輯分析協議 64
4.4 時態邏輯 69
4.4.1 Kripke結構 70
4.4.2 CTL*、CTL和LTL 70
4.4.3 并發系統性質描述 72
4.4.4 實例 73
4.5 形式化分析流程 74
4.5.1 形式化建模 75
4.5.2 協議安全性質刻畫 79
4.5.3 形式化驗證 79
4.6 驗證模型優化策略 79
4.6.1 靜態分析 79
4.6.2 語法重定序 84
4.6.3 偏序歸約 84
4.6.4 優化策略對比 87
4.7 與其他方法對比 88
4.7.1 與認證邏輯對比 89
4.7.2 與FDR對比 91
4.7.3 與Murφ對比 93
4.7.4 與NRL協議分析器對比 95
4.7.5 與Athena對比 97
4.7.6 與Isabelle對比 100
4.7.7 與BRUTUS對比 101
參考文獻 103
第5章 網絡安全協議驗證模型生成系統 108
5.1 系統概述 108
5.1.1 系統簡介 108
5.1.2 系統功能 110
5.2 系統設計與實現 112
5.2.1 整體設計 112
5.2.2 模塊設計 112
5.2.3 協議描述語言ProDL 124
5.2.4 Needham-Schroeder公開密鑰協議分析與驗證 130
5.2.5 BAN-Yahalom三方對稱密鑰認證協議分析與驗證 132
5.2.6 CMP1可信第三方電子商務協議分析與驗證 133
參考文獻 135
第6章 基于事件邏輯的安全協議形式化分析 137
6.1 事件系統 137
6.1.1 符號說明 137
6.1.2 消息自動機 138
6.1.3 語法語義 139
6.1.4 不可猜測的原子 140
6.1.5 事件結構 140
6.1.6 事件類 142
6.2 事件邏輯公理、推論及性質 143
6.2.1 事件邏輯公理 143
6.2.2 事件邏輯推論及性質 146
6.3 事件邏輯形式化描述協議 147
6.4 基于事件邏輯的安全協議證明 150
6.4.1 推理規則 150
6.4.2 兩方安全協議證明流程 151
6.4.3 三方安全協議證明流程 153
6.5 與其他典型證明方法對比 154
6.5.1 PCL 154
6.5.2 BAN類邏輯 155
6.5.3 串空間理論 155
參考文獻 156
第7章 總結與展望 158
7.1 研究成果總結 158
7.2 下一步研究工作 159
前言
第1章 緒論 1
1.1 安全協議形式化分析背景 1
1.2 安全協議形式化分析研究現狀 3
參考文獻 6
第2章 形式化方法基本理論 10
2.1 形式化方法概述 10
2.2 模態邏輯 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協議分析器 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
參考文獻 36
第3章 安全協議 39
3.1 安全協議概念 39
3.2 安全協議分類 40
3.2.1 ISO/IEC 11770-2密鑰建立機制6協議 40
3.2.2 NSSK協議 41
3.2.3 Kerberos認證協議 42
3.2.4 ISO/IEC 9798-3協議 44
3.2.5 NSPK協議 44
3.3 協議安全屬性 45
3.4 協議安全構建方法 46
3.4.1 Hash函數 48
3.4.2 隨機數 49
3.4.3 時間戳 50
3.5 協議攻擊者模型及其攻擊類型 51
3.5.1 Dolev-Yao攻擊者模型 52
3.5.2 攻擊類型 53
參考文獻 53
第4章 基于模型檢測的安全協議分析 55
4.1 安全協議形式化表示 55
4.1.1 原子消息(基本約定) 55
4.1.2 消息 55
4.1.3 動作 56
4.1.4 協議 57
4.1.5 跡 57
4.2 消息生成規則 58
4.3 基于算法知識邏輯的協議形式化分析 61
4.3.1 多智體系統 62
4.3.2 算法知識邏輯 62
4.3.3 算法知識邏輯分析協議 64
4.4 時態邏輯 69
4.4.1 Kripke結構 70
4.4.2 CTL*、CTL和LTL 70
4.4.3 并發系統性質描述 72
4.4.4 實例 73
4.5 形式化分析流程 74
4.5.1 形式化建模 75
4.5.2 協議安全性質刻畫 79
4.5.3 形式化驗證 79
4.6 驗證模型優化策略 79
4.6.1 靜態分析 79
4.6.2 語法重定序 84
4.6.3 偏序歸約 84
4.6.4 優化策略對比 87
4.7 與其他方法對比 88
4.7.1 與認證邏輯對比 89
4.7.2 與FDR對比 91
4.7.3 與Murφ對比 93
4.7.4 與NRL協議分析器對比 95
4.7.5 與Athena對比 97
4.7.6 與Isabelle對比 100
4.7.7 與BRUTUS對比 101
參考文獻 103
第5章 網絡安全協議驗證模型生成系統 108
5.1 系統概述 108
5.1.1 系統簡介 108
5.1.2 系統功能 110
5.2 系統設計與實現 112
5.2.1 整體設計 112
5.2.2 模塊設計 112
5.2.3 協議描述語言ProDL 124
5.2.4 Needham-Schroeder公開密鑰協議分析與驗證 130
5.2.5 BAN-Yahalom三方對稱密鑰認證協議分析與驗證 132
5.2.6 CMP1可信第三方電子商務協議分析與驗證 133
參考文獻 135
第6章 基于事件邏輯的安全協議形式化分析 137
6.1 事件系統 137
6.1.1 符號說明 137
6.1.2 消息自動機 138
6.1.3 語法語義 139
6.1.4 不可猜測的原子 140
6.1.5 事件結構 140
6.1.6 事件類 142
6.2 事件邏輯公理、推論及性質 143
6.2.1 事件邏輯公理 143
6.2.2 事件邏輯推論及性質 146
6.3 事件邏輯形式化描述協議 147
6.4 基于事件邏輯的安全協議證明 150
6.4.1 推理規則 150
6.4.2 兩方安全協議證明流程 151
6.4.3 三方安全協議證明流程 153
6.5 與其他典型證明方法對比 154
6.5.1 PCL 154
6.5.2 BAN類邏輯 155
6.5.3 串空間理論 155
參考文獻 156
第7章 總結與展望 158
7.1 研究成果總結 158
7.2 下一步研究工作 159
展開全部
書友推薦
- >
月亮與六便士
- >
巴金－再思錄
- >
推拿
- >
經典常談
- >
史學評論
- >
中國人在烏蘇里邊疆區:歷史與人類學概述
- >
回憶愛瑪儂
- >
隨園食單
本類暢銷
