安全協(xié)議實(shí)施安全性自動(dòng)化分析與驗(yàn)證

目錄
第1章 安全協(xié)議實(shí)施安全性分析與驗(yàn)證現(xiàn)狀 1
1.1 引言 1
1.2 能夠獲取安全協(xié)議客戶端實(shí)施和安全協(xié)議服務(wù)器端實(shí)施 1
1.2.1 程序驗(yàn)證 1
1.2.2 模型抽取 3
1.3 僅能夠獲取安全協(xié)議客戶端實(shí)施 6
1.3.1 網(wǎng)絡(luò)軌跡 6
1.3.2 模型抽取 8
1.4 不能獲取安全協(xié)議客戶端實(shí)施和安全協(xié)議服務(wù)器端實(shí)施 10
1.4.1 指令序列 11
1.4.2 網(wǎng)絡(luò)軌跡 16
1.4.3 流量識別 20
參考文獻(xiàn) 39
第2章 Applied PI演算與其BNF范式 51
2.1 引言 51
2.2 Applied PI演算語法及語義 51
2.3 Applied PI演算BNF范式 55
參考文獻(xiàn) 58
第3章 一階定理證明器ProVerif及應(yīng)用 59
3.1 引言 59
3.2 一階定理證明器ProVerif 59
3.3 ProVerif的輸入和輸出 63
3.4 自動(dòng)化分析OpenID Connect安全協(xié)議安全性 64
3.4.1 OpenID Connect安全協(xié)議 64
3.4.2 應(yīng)用Applied PI演算對OpenID Connect安全協(xié)議形式化建模 67
3.4.3 利用Proverif驗(yàn)證OpenID Connect安全協(xié)議秘密性和認(rèn)證性 70
3.4.4 分析結(jié)果 72
3.5 自動(dòng)化分析PPMUAS身份認(rèn)證協(xié)議安全性 73
3.5.1 PPMUAS身份認(rèn)證協(xié)議 73
3.5.2 應(yīng)用Applied PI演算對PPMUAS身份認(rèn)證協(xié)議形式化建模 75
3.5.3 利用Proverif驗(yàn)證PPUMAS身份認(rèn)證協(xié)議秘密性和認(rèn)證性 78
3.5.4 分析結(jié)果 78
3.6 自動(dòng)化分析改進(jìn)的OpenID Connect安全協(xié)議認(rèn)證性 81
3.6.1 改進(jìn)的OpenID Connect安全協(xié)議 81
3.6.2 應(yīng)用Applied PI演算對改進(jìn)的OpenID Connect安全協(xié)議形式化建模 83
3.6.3 利用ProVerif驗(yàn)證改進(jìn)的OpenID Connect安全協(xié)議認(rèn)證性 87
3.6.4 分析結(jié)果 87
3.7 自動(dòng)化分析Mynah安全協(xié)議認(rèn)證性 91
3.7.1 Mynah安全協(xié)議 91
3.7.2 應(yīng)用Applied PI演算對Mynah安全協(xié)議形式化建模 93
3.7.3 利用ProVerif驗(yàn)證Mynah安全協(xié)議認(rèn)證性 95
3.7.4 分析結(jié)果 96
參考文獻(xiàn) 97
第4章 概率進(jìn)程演算Blanchet演算與其BNF范式 99
4.1 引言 99
4.2 Blanchet演算語法及語義 99
4.3 Blanchet演算BNF范式 106
參考文獻(xiàn) 109
第5章 自動(dòng)化安全協(xié)議證明器CryptoVerif及應(yīng)用 110
5.1 引言 110
5.2 自動(dòng)化安全協(xié)議證明器CryptoVerif 110
5.2.1 結(jié)構(gòu) 110
5.2.2 證明目標(biāo) 115
5.2.3 語法 117
5.3 自動(dòng)化分析TLS 1.3 握手協(xié)議安全性 119
5.3.1 TLS 1.3 握手協(xié)議 119
5.3.2 應(yīng)用Blanchet演算對TLS 1.3 握手協(xié)議形式化建模 121
5.3.3 利用CryptoVerif驗(yàn)證TLS 1.3 握手協(xié)議的秘密性和認(rèn)證性 127
5.3.4 分析結(jié)果 131
參考文獻(xiàn) 133
第6章 自動(dòng)化抽取安全協(xié)議Blanchet演算實(shí)施模型 135
6.1 引言 135
6.2 Swift語言子集SubSwift語言及其BNF范式 136
6.3 Swift語言到Blanchet演算映射模型 139
6.4 Swift語言到Blanchet演算語句映射關(guān)系 141
6.5 Swift語言類型到Blanchet演算類型映射關(guān)系 144
參考文獻(xiàn) 144
第7章 安全協(xié)議抽象規(guī)范模型生成工具Swift2CV 146
7.1 引言 146
7.2 Swift2CV架構(gòu) 146
7.3 Swift2CV詞法分析器 149
7.4 Swift2CV語法分析器 154
7.5 Swift2CV語法樹遍歷器 157
7.6 Swift2CV語法樹注解器 163
7.7 Swift2CV使用手冊 165
參考文獻(xiàn) 166
第8章 典型安全協(xié)議Swift實(shí)施安全性分析 167
8.1 引言 167
8.2 OpenID Connect協(xié)議Swift實(shí)施安全性 168
8.2.1 OpenID Connect協(xié)議Swift實(shí)施 168
8.2.2 OpenID Connect協(xié)議Blanchet實(shí)施 171
8.3 Oauth2.0 協(xié)議Swift實(shí)施安全性 173
8.4 TLS1.2 協(xié)議Swift實(shí)施安全性 174
參考文獻(xiàn) 175
第9章 基于消息構(gòu)造的安全協(xié)議實(shí)施安全性分析 176
9.1 引言 176
9.2 基于API trace的安全協(xié)議消息構(gòu)造方法 177
9.2.1 Net-trace解析 178
9.2.2 API trace解析 180
9.2.3 Token定位 181
9.2.4 安全函數(shù)重構(gòu)與消息構(gòu)造 183
9.3 安全協(xié)議服務(wù)器端抽象模型生成 185
9.3.1 安全協(xié)議服務(wù)器端響應(yīng)消息解析 185
9.3.2 安全協(xié)議服務(wù)器端抽象模型生成方法 186
9.4 基于消息構(gòu)造的安全協(xié)議實(shí)施安全性分析方法 189
參考文獻(xiàn) 191
第10章 安全協(xié)議實(shí)施安全性分析工具SPISA 192
10.1 引言 192
10.2 SPISA架構(gòu) 193
10.3 SPISA Net-trace解析器 194
10.4 SPISA API trace解析器 195
10.5 SPISA Token定位器 196
10.6 SPISA安全函數(shù)重構(gòu)器 197
10.7 SPISA服務(wù)器端模型生成器 198
10.8 SPISA測試 199
參考文獻(xiàn) 200
第11章 典型認(rèn)證系統(tǒng)安全性分析 201
11.1 引言 201
11.2 RSAAuth認(rèn)證系統(tǒng)安全性分析 203
11.2.1 請求消息構(gòu)造 203
11.2.2 服務(wù)器端抽象模型生成 206
11.2.3 分析結(jié)果 207
11.3 騰訊QQ郵件認(rèn)證系統(tǒng)安全性分析 207
參考文獻(xiàn) 208
第12章 基于網(wǎng)絡(luò)軌跡的安全協(xié)議實(shí)施安全性分析 209
12.1 引言 209
12.2 安全協(xié)議實(shí)施本體架構(gòu) 210
12.3 面向多個(gè)混合安全協(xié)議軌跡的安全協(xié)議格式逆向分析 212
12.3.1 軌跡分割 213
12.3.2 IF分布擬合 214
12.3.3 IF分類 214
12.3.4 軌跡聚類 216
12.3.5 格式推斷 216
12.4 安全協(xié)議軌跡到安全協(xié)議實(shí)施本體的映射方法 216
12.4.1 預(yù)處理 218
12.4.2 Token匹配 218
12.4.3 Msg匹配方法 218
12.4.4 Flow匹配方法 220
12.5 基于網(wǎng)絡(luò)軌跡的安全協(xié)議實(shí)施安全性分析方法 221
12.6 討論 223
參考文獻(xiàn) 224
第13章 安全協(xié)議實(shí)施安全性分析工具NTISA 226
13.1 引言 226
13.2 NTISA架構(gòu) 226
13.3 格式解析器FA 227
13.3.1 Token分割模塊 227
13.3.2 曲線擬合模塊 228
13.3.3 字符分類模塊 229
13.3.4 軌跡分類模塊 229
13.3.5 協(xié)議格式推斷模塊 230
13.4 語義解析器SA 230
13.4.1 安全協(xié)議實(shí)施本體模塊 231
13.4.2 Token匹配模塊 231
13.4.3 Msg匹配模塊 232
12.4.4 Flow匹配模塊 233
13.5 實(shí)施安全分析器ISA 233
13.5.1 軌跡標(biāo)記模塊 234
13.5.2 映射分析模塊 234
13.5.3 非本體Token分析模塊 235
參考文獻(xiàn) 235
第14章 某認(rèn)證平臺安全協(xié)議實(shí)施安全性分析 236
14.1 引言 236
14.2 數(shù)據(jù)獲取 236
14.3 格式解析 237
14.3.1 Token分割 237
14.3.2 曲線擬合 237
14.3.3 字符與軌跡分類 238
14.3.4 協(xié)議格式推斷 239
14.3.5 語義解析 241
14.3.6 安全協(xié)議實(shí)施本體構(gòu)造 242
14.3.7 Token權(quán)值計(jì)算 243
14.3.8 Msg匹配 245
14.3.9 Flow匹配 246
14.4 分析結(jié)果 248
參考文獻(xiàn) 249