安全協(xié)議實施安全性自動化分析與驗證

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