●第1章 安全協議實施安全性分析與驗證現狀
1.1 引言
1.2 能夠獲取安全協議客戶端實施和安全協議服務器端實施
1.2.1 程序驗證
1.2.2 模型抽取
1.3 僅能夠獲取安全協議客戶端實施
1.3.1 網絡軌跡
1.3.2 模型抽取
1.4 不能獲取安全協議客戶端實施和安全協議服務器端實施
1.4.1 指令序列
1.4.2 網絡軌跡
1.4.3 流量識別
參考文獻
第2章 Applied PI演算與其BNF範式
2.1 引言
2.2 Applied PI演算語法及語義
2.3 Applied PI演算BNF範式
參考文獻
第3章 一階定理證明器ProVerif及應用
3.1 引言
3.2 一階定理證明器ProVerif
3.3 ProVerif的輸入和輸出
3.4 自動化分析OpenID Connect安全協議安全性
3.4.1 OpenID Connect安全協議
3.4.2 應用Applied PI演算對OpenID Connect安全協議形式化建模
3.4.3 利用Proverif驗證OpenID Connect安全協議秘密性和認證性
3.4.4 分析結果
3.5 自動化分析PPMUAS身份認證協議安全性
3.5.1 PPMUAS身份認證協議
3.5.2 應用Applied PI演算對PPMUAS身份認證協議形式化建模
3.5.3 利用Proverif驗證PPMUAS身份認證協議秘密性和認證性
3.5.4 分析結果
3.6 自動化分析改進的OpenID Connect安全協議認證性
3.6.1 改進的OpenID Connect安全協議
3.6.2 應用Applied PI演算對改進的0penID Connect安全協議形式化建模
3.6.3 利用ProVerif驗證改進的OpenID Connect安全協議認證性
3.6.4 分析結果
3.7 自動化分析Mynah安全協議認證性
3.7.1 Mynah安全協議
3.7.2 應用Applied PI演算對Mynah安全協議形式化建模
3.7.3 利用ProVerif驗證Mynah安全協議認證性
3.7.4 分析結果
參考文獻
第4章 概率進程演算Blanchet演算與其BNF範式
4.1 引言
4.2 Blanchet演算語法及語義
4.3 Blanchet演算BNF範式
參考文獻
第5章 自動化安全協議證明器CryptoVerif及應用
5.1 引言
5.2 自動化安全協議證明器CryptoVerif
5.2.1 結構
5.2.2 證明目標
5.2.3 語法
5.3 自動化分析TLS 1.3握手協議安全性
5.3.1 TLS 1.3握手協議
5.3.2 應用Blanchet演算對TLS 1.3握手協議形式化建模
5.3.3 利用Crypto Verif驗證TLS 1.3握手協議的秘密性和認證性
5.3.4 分析結果
參考文獻
第6章 自動化抽取安全協議Blanchet演算實施模型
6.1 引言
6.2 Swift語言子集SubSwift語言及其BNF範式
6.3 Swift語言到Blanchet演算映射模型
6.4 Swift語言到Blanchet演算語句映射關繫
6.5 Swift語言類型到Blanchet演算類型映射關繫
參考文獻
第7章 安全協議抽像規範模型生成工具Swift2CV
7.1 引言
7.2 Swift2CV架構
7.3 Swift2CV詞法分析器
7.4 Swift2CV語法分析器
7.5 Swift2CV語法樹遍歷器
7.6 Swift2CV語法樹注解器
7.7 Swift2CV使用手冊
參考文獻
第8章 典型安全協議Swift實施安全性分析
8.1 引言
8.2 OpenID Connect協議Swift實施安全性
8.2.1 OpenID Connect協議Swift實施
8.2.2 OpenID Connect協議Blanchet實施
8.3 Oauth2.0協議Swift實施安全性
8.4 TLS1.2協議Swift實施安全性
參考文獻
第9章 基於消息構造的安全協議實施安全性分析
9.1 引言
9.2 基於API trace的安全協議消息構造方法
9.2.1 Net-trace解析
9.2.2 API trace解析
9.2.3 Token定位
9.2.4 安全函數重構與消息構造
9.3 安全協議服務器端抽像模型生成
9.3.1 安全協議服務器端響應消息解析
9.3.2 安全協議服務器端抽像模型生成方法
9.4 基於消息構造的安全協議實施安全性分析方法
參考文獻
第10章 安全協議實施安全性分析工具SPISA
10.1 引言
10.2 SPISA架構
10.3 SPISA Net-trace解析器
10.4 SPISA API trace解析器
10.5 SPISA Token定位器
10.6 SPISA安全函數重構器
10.7 SPISA服務器端模型生成器
10.8 SPISA測試
參考文獻
第11章 典型認證繫統安全性分析
11.1 引言
11.2 RSAAuth認證繫統安全性分析
11.2.1 請求消息構造
11.2.2 服務器端抽像模型生成
11.2.3 分析結果
11.3 騰訊QQ郵件認證繫統安全性分析
參考文獻
第12章 基於網絡軌跡的安全協議實施安全性分析
12.1 引言
12.2 安全協議實施本體架構
12.3 面向多個混合安全協議軌跡的安全協議格式逆向分析
12.3.1 軌跡分割
12.3.2 IF分布擬合
12.3.3 IF分類
12.3.4 軌跡聚類
12.3.5 格式推斷
12.4 安全協議軌跡到安全協議實施本體的映射方法
12.4.1 預處理
12.4.2 Token匹配
12.4.3 Msg匹配方法
12.4.4 Flow匹配方法
12.5 基於網絡軌跡的安全協議實施安全性分析方法
12.6 討論
參考文獻
第13章 安全協議實施安全性分析工具NTISA
13.1 引言
13.2 NTISA架構
13.3 格式解析器FA
13.3.1 Token分割模塊
13.3.2 曲線擬合模塊
13.3.3 字符分類模塊
13.3.4 軌跡分類模塊
13.3.5 協議格式推斷模塊
13.4 語義解析器SA
13.4.1 安全協議實施本體模塊
13.4.2 Token匹配模塊
13.4.3 Msg匹配模塊
12.4.4 Flow匹配模塊
13.5 實施安全分析器ISA
13.5.1 軌跡標記模塊
13.5.2 映射分析模塊
13.5.3 非本體Token分析模塊
參考文獻
第14章 某認證平臺安全協議實施安全性分析
14.1 引言
14.2 數據獲取
14.3 格式解析
14.3.1 Token分割
14.3.2 曲線擬合
14.3.3 字符與軌跡分類
14.3.4 協議格式推斷
14.3.5 語義解析
14.3.6 安全協議實施本體構造
14.3.7 Token權值計算
14.3.8 Msg匹配
14.3.9 Flow匹配
14.4 分析結果
參考文獻

《安全協議實施安全性自動化分析與驗證》繫統介紹安全協議實施安全性自動化分析與驗證的基本理論和關鍵技術及新成果。《安全協議實施安全性自動化分析與驗證》主要內容包括安全協議實施安全性分析與驗證的國內外發展現狀、一階定理證明器ProVerif及應用、自動化安全協議證明器CryptoVerif及應用、基於計算模型自動化抽取安全協議Blanchet演算實施模型、安全協議Blanchet演算實施自動化抽取工具Swift2CV、基於消息構造的安全協議實施安全性分析方法、安全協議實施安全性分析工具SPISA、面向多個混合安全協議軌跡的安全協議實施安全性分析方法、安全協議實施安全性分析工具NTISA、典型安全協議實施安全性分析等。《安全協議實施安全性自動化分析與驗證》可供從事安全協議、密碼學、計算機、軟件工程、通信、數學等專業的科技人員、碩士和博士研究生參考，也可供高等院校相關專業的師生參考。