《安全協定操作語義與驗證》是2018年11月電子工業出版社出版的圖書，作者是吳漢煒。
基本介紹
- 書名：安全協定操作語義與驗證
- 作者：吳漢煒
- ISBN：9787121351952
- 頁數：148頁
- 定價：59元
- 出版社：電子工業出版社
- 出版時間：2018年11月
- 開本：16開
內容簡介,圖書目錄,
內容簡介
安全協定作為信息安全的重要基礎之一，其安全屬性能否達到設計者的初始目標成為一個重要研究內容，關係到依賴於協定的上層套用系統的安全性。本書的內容主要涵蓋兩部分：用形式化的語義定義協殃宙擊鑽議的執行規格和安全屬性，精確表示安全協定的安全屬性；綜合運用各種形式化方法設計一個高效的驗證算法，在可接受的時間內驗證安全屬性。本書還探討了多協定安全分析，比較分析了各種驗證理論和發展趨勢。
圖書目錄
目 錄
第1章 背景介紹 1
1.1 歷史背景 1
1.2 基於黑盒的安全協定分析 3
1.3 目的與方法 5
1.4 概要 5
1.4.1 協定分析模型 6
1.4.2 模型的套用 6
第2章 預備知識 7
2.1 集合與關係 7
2.2 巴科斯範式 8
2.3 符號變遷系統 8
第3章 操作語義 10
3.1 問題域分析 10
3.2 安全協定規範 13
3.2.1 角色項 14
3.2.2 協定規範 16
3.2.3 事件次序 18
3.3 協定執行描繪 20
3.3.1 回合 20
3.3.2 匹配 21
3.3.3 回合事件 23
3.3.4 威脅模型 24
3.4 操作語義 25
3.5 協邀棗乃議規範實例 27
3.6 思考題 28
第4章 安全屬性 29
4.1 安全斷言事件屬恥催凝性 29
4.2 機密性 30
4.3 認證酷重料 32
4.3.1 存活性 32
4.3.2 同再葛步一致性 35
4.3.3 非單射同步一致性 37
4.3.4 單射同步一致性 38
4.3.5 訊息一致性 39
4.4 認證繼承關係 41
4.5 對NS協定的攻擊和改進 44
4.6 總結 49
4.7 思考題 50
第5章 驗證 52
5.1 模式 52
5.2 驗證算法 58
5.2.1 良構模式 59
5.2.2 可達模式 59
5.2.3 空模式和冗餘模式 60
5.2.4 算法概述 61
5.2.5 模式精煉 62
5.3 搜尋空間遍歷實例 66
5.4 使用模式精煉驗證安全屬性 70
5.5 啟發式算法和參數選擇 71
5.5.1 啟發式算法 71
5.5.2 選擇一個合適的回合數 74
5.5.3 性能 75
5.6 驗證單射性 76
5.6.1 單射同步一致性 76
5.6.2 LOOP循環屬性 79
5.6.3 模型假設 82
5.7 更多Scyther分析系統的特性 82
5.8 思考題 84
第6章 多協定攻擊 85
6.1 多協定攻擊概述 86
6.2 實驗 86
6.3 測試結果 87
6.3.1 嚴格類型匹配：無類型缺陷 89
6.3.2 簡單類型匹配：基本類型缺陷 90
6.3.3 無類型匹配：所有類型缺陷 90
6.3.4 攻擊例子 90
6.4 攻擊場景 92
6.4.1 協定更新 92
6.4.2 歧義性身份驗證 94
6.5 預防多促祝謎協定攻擊 96
6.6 總結 97
6.7 思考題 97
第7章 基於NSL擴展的多方認證 98
7.1 一個多方身份認證協定 98
7.2 安全分析 101
7.2.1 初步檢測 101
7.2.2 正確性證明 102
7.2.3 角色 的隨機數機密性 105
7.2.4 初始化角色 的非單射同步一致性 106
7.2.5 非初始化角色 的隨機數機密性 107
7.2.6 非初始化角色 的非單射同備辯陵察步一致性 107
7.2.7 所有角色的單射同步一致性 108
7.2.8 類型缺陷攻擊 108
7.2.9 訊息最小化 108
7.3 模式變體 109
7.4 弱多方認證協定 111
7.5 思考題 112
第8章 歷史背景和進階閱讀 114
8.1 歷史背景 114
8.1.1 模型 114
8.1.2 早期分析工具 114
8.1.3 邏輯 114
8.1.4 驗證工具 115
8.1.5 多協定攻擊 117
8.1.6 複雜度分析 117
8.1.7 符號化模型和計算模型之間的差異 117
8.1.8 消除安全分析和代碼實現之間的差異 118
8.2 可選方法 119
8.2.1 建模框架 119
8.2.2 安全屬性 120
8.2.3 驗證工具 122
參考文獻 125
5.5.3 性能 75
5.6 驗證單射性 76
5.6.1 單射同步一致性 76
5.6.2 LOOP循環屬性 79
5.6.3 模型假設 82
5.7 更多Scyther分析系統的特性 82
5.8 思考題 84
第6章 多協定攻擊 85
6.1 多協定攻擊概述 86
6.2 實驗 86
6.3 測試結果 87
6.3.1 嚴格類型匹配：無類型缺陷 89
6.3.2 簡單類型匹配：基本類型缺陷 90
6.3.3 無類型匹配：所有類型缺陷 90
6.3.4 攻擊例子 90
6.4 攻擊場景 92
6.4.1 協定更新 92
6.4.2 歧義性身份驗證 94
6.5 預防多協定攻擊 96
6.6 總結 97
6.7 思考題 97
第7章 基於NSL擴展的多方認證 98
7.1 一個多方身份認證協定 98
7.2 安全分析 101
7.2.1 初步檢測 101
7.2.2 正確性證明 102
7.2.3 角色 的隨機數機密性 105
7.2.4 初始化角色 的非單射同步一致性 106
7.2.5 非初始化角色 的隨機數機密性 107
7.2.6 非初始化角色 的非單射同步一致性 107
7.2.7 所有角色的單射同步一致性 108
7.2.8 類型缺陷攻擊 108
7.2.9 訊息最小化 108
7.3 模式變體 109
7.4 弱多方認證協定 111
7.5 思考題 112
第8章 歷史背景和進階閱讀 114
8.1 歷史背景 114
8.1.1 模型 114
8.1.2 早期分析工具 114
8.1.3 邏輯 114
8.1.4 驗證工具 115
8.1.5 多協定攻擊 117
8.1.6 複雜度分析 117
8.1.7 符號化模型和計算模型之間的差異 117
8.1.8 消除安全分析和代碼實現之間的差異 118
8.2 可選方法 119
8.2.1 建模框架 119
8.2.2 安全屬性 120
8.2.3 驗證工具 122
參考文獻 125
