安全協議操作語義與驗證

第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