安全協(xié)議操作語(yǔ)義與驗(yàn)證

第1章  背景介紹 1

1.1  歷史背景 1

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

1.3  目的與方法 5

1.4  概要 5

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

1.4.2  模型的應(yīng)用 6

第2章  預(yù)備知識(shí) 7

2.1  集合與關(guān)系 7

2.2  巴科斯范式 8

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

第3章  操作語(yǔ)義 10

3.1  問(wèn)題域分析 10

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

3.2.1  角色項(xiàng) 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  操作語(yǔ)義 25

3.5  協(xié)議規(guī)范實(shí)例 27

3.6  思考題 28

第4章  安全屬性 29

4.1  安全斷言事件屬性 29

4.2  機(jī)密性 30

4.3  認(rèn)證 32

4.3.1  存活性 32

4.3.2  同步一致性 35

4.3.3  非單射同步一致性 37

4.3.4  單射同步一致性 38

4.3.5  消息一致性 39

4.4  認(rèn)證繼承關(guān)系 41

4.5  對(duì)NS協(xié)議的攻擊和改進(jìn) 44

4.6  總結(jié) 49

4.7  思考題 50

第5章  驗(yàn)證 52

5.1  模式 52

5.2  驗(yàn)證算法 58

5.2.1  良構(gòu)模式 59

5.2.2  可達(dá)模式 59

5.2.3  空模式和冗余模式 60

5.2.4  算法概述 61

5.2.5  模式精煉 62

5.3  搜索空間遍歷實(shí)例 66

5.4  使用模式精煉驗(yàn)證安全屬性 70

5.5  啟發(fā)式算法和參數(shù)選擇 71

5.5.1  啟發(fā)式算法 71

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

5.5.3  性能 75

5.6  驗(yàn)證單射性 76

5.6.1  單射同步一致性 76

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

5.6.3  模型假設(shè) 82

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

5.8  思考題 84

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

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

6.2  實(shí)驗(yàn) 86

6.3  測(cè)試結(jié)果 87

6.3.1  嚴(yán)格類型匹配：無(wú)類型缺陷 89

6.3.2  簡(jiǎn)單類型匹配：基本類型缺陷 90

6.3.3  無(wú)類型匹配：所有類型缺陷 90

6.3.4  攻擊例子 90

6.4  攻擊場(chǎng)景 92

6.4.1  協(xié)議更新 92

6.4.2  歧義性身份驗(yàn)證 94

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

6.6  總結(jié) 97

6.7  思考題 97

第7章  基于NSL擴(kuò)展的多方認(rèn)證 98

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

7.2  安全分析 101

7.2.1  初步檢測(cè) 101

7.2.2  正確性證明 102

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

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

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

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

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

7.2.8  類型缺陷攻擊 108

7.2.9  消息最小化 108

7.3  模式變體 109

7.4  弱多方認(rèn)證協(xié)議 111

7.5  思考題 112

第8章  歷史背景和進(jìn)階閱讀 114

8.1  歷史背景 114

8.1.1  模型 114

8.1.2  早期分析工具 114

8.1.3  邏輯 114

8.1.4  驗(yàn)證工具 115

8.1.5  多協(xié)議攻擊 117

8.1.6  復(fù)雜度分析 117

8.1.7  符號(hào)化模型和計(jì)算模型之間的差異 117

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

8.2  可選方法 119

8.2.1  建?？蚣?119

8.2.2  安全屬性 120

8.2.3  驗(yàn)證工具 122

參考文獻(xiàn) 125