安全協(xié)議操作語義與驗證

第1章  背景介紹 1

1.1  歷史背景 1

1.2  基于黑盒的安全協(xié)議分析 3

1.3  目的與方法 5

1.4  概要 5

1.4.1  協(xié)議分析模型 6

1.4.2  模型的應用 6

第2章  預備知識 7

2.1  集合與關系 7

2.2  巴科斯范式 8

2.3  符號變遷系統(tǒng) 8

第3章  操作語義 10

3.1  問題域分析 10

3.2  安全協(xié)議規(guī)范 13

3.2.1  角色項 14

3.2.2  協(xié)議規(guī)范 16

3.2.3  事件次序 18

3.3  協(xié)議執(zhí)行描繪 20

3.3.1  回合 20

3.3.2  匹配 21

3.3.3  回合事件 23

3.3.4  威脅模型 24

3.4  操作語義 25

3.5  協(xié)議規(guī)范實例 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協(xié)議的攻擊和改進 44

4.6  總結(jié) 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  啟發(fā)式算法和參數(shù)選擇 71

5.5.1  啟發(fā)式算法 71

5.5.2  選擇一個合適的回合數(shù) 74

5.5.3  性能 75

5.6  驗證單射性 76

5.6.1  單射同步一致性 76

5.6.2  LOOP循環(huán)屬性 79

5.6.3  模型假設 82

5.7  更多Scyther分析系統(tǒng)的特性 82

5.8  思考題 84

第6章  多協(xié)議攻擊 85

6.1  多協(xié)議攻擊概述 86

6.2  實驗 86

6.3  測試結(jié)果 87

6.3.1  嚴格類型匹配：無類型缺陷 89

6.3.2  簡單類型匹配：基本類型缺陷 90

6.3.3  無類型匹配：所有類型缺陷 90

6.3.4  攻擊例子 90

6.4  攻擊場景 92

6.4.1  協(xié)議更新 92

6.4.2  歧義性身份驗證 94

6.5  預防多協(xié)議攻擊 96

6.6  總結(jié) 97

6.7  思考題 97

第7章  基于NSL擴展的多方認證 98

7.1  一個多方身份認證協(xié)議 98

7.2  安全分析 101

7.2.1  初步檢測 101

7.2.2  正確性證明 102

7.2.3  角色 的隨機數(shù)機密性 105

7.2.4  初始化角色 的非單射同步一致性 106

7.2.5  非初始化角色 的隨機數(shù)機密性 107

7.2.6  非初始化角色 的非單射同步一致性 107

7.2.7  所有角色的單射同步一致性 108

7.2.8  類型缺陷攻擊 108

7.2.9  消息最小化 108

7.3  模式變體 109

7.4  弱多方認證協(xié)議 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  多協(xié)議攻擊 117

8.1.6  復雜度分析 117

8.1.7  符號化模型和計算模型之間的差異 117

8.1.8  消除安全分析和代碼實現(xiàn)之間的差異 118

8.2  可選方法 119

8.2.1  建?？蚣?119

8.2.2  安全屬性 120

8.2.3  驗證工具 122

參考文獻 125