《安全協議實施自動化生成與驗證》包括五篇，共15章。系統地全面介紹了安全實施自動化生成與驗證的基本理論和關鍵技術及新成果。主要內容包括安全協議規范與實施的形式化分析與驗證的國內外發展現狀、基于計算模型自動化抽取安全協議Blanchet演算實施模型、安全協議Blanchet演算實施自動化抽取工具JAVA2CV、基于計算模型自動化生成安全協議Java實施模型、安全協議Java實施自動化生成工具CV2JAVA、基于符號模型自動化生成安全協議Java實施模型、安全協議Java實施自動化生成工具PV2JAVA、典型安全協議Java實施生成與驗證等。
《安全協議實施自動化生成與驗證》可供從事安全協議、密碼學、計算機、軟件工程、通信、數學等專業的科技人員、碩士和博士研究生參考，也可供高等院校相關專業的師生參考。
第一篇 安全協議規范及實施形式化分析與驗證
第1章 安全協議規范形式化分析與驗證發展現狀
1．1 引言
1．2 符號模型
1．3 計算模型
1．4 本章小結
參考文獻
第2章 安全協議實施生成與驗證發展現狀
2．1 引言
2．2 模型抽取：驗證安全協議實施
2．2．1 程序驗證
2．2．2 模型抽取
2．3 代碼生成：生成安全協議實施
2．4 安全協議實施生成與驗證模型
2．4．1 安全協議實施模型抽取
2．4．2 安全協議實施生成
2．5 本章小結
參考文獻
第二篇 安全協議規范形式化分析與驗證
第3章 AppliedPI演算與其BNF范式
3．1 引言
3．2 AppliedPI演算
3．3 AppliedPI演算BNF范式
3．4 本章小結
參考文獻
第4章 一階定理證明器ProVerif及應用
4．1 引言
4．2 一階定理證明器ProVerif
4．3 ProVerif的輸入和輸出
4．4 自動化分析基于SAML2．0的聯合身份認證協議安全性
4．4．1 基于SAML2．0的聯合身份認證協議
4．4．2 應用AppliedPI演算對基于SAML2．0的聯合身份認證協議形式化建模
4．4．3 利用ProVerif驗證基于SAML2．0的聯合身份認證協議的秘密性和認證性
4．4．4 分析結果
4．5 本章小結
參考文獻
第5章 概率進程演算Blanchet演算與其BNF范式
5．1 引言
5．2 Blanchet演算
5．3 Blanchet演算BNF范式
5．4 本章小結
參考文獻
第6章 自動化安全協議證明器CryptoVerif及應用
6．1 引言
6．2 自動化安全協議證明器CryptoVerif
6．2．1 結構
6．2．2 證明目標
6．2．3 語法
6．3 自動化分析OpenIDConnect安全協議認證性
6．3．1 0penIDConnect安全協議
6．3．2 應用Blanchet演算對OpenIDConnect安全協議形式化建模
6．3．3 利用CryptoVerif驗證OpenIDConnect安全協議的認證性
6．3．4 分析結果
6．4 自動化分析改進的OAuth2．0安全協議認證性
6．4．1 改進的OAuth2．0安全協議
6．4．2 應用Blanchet演算對改進的OAuth2．0安全協議形式化建模
6．4．3 利用CryptoVerif驗證改進的OAuth2．0安全協議的認證性
6．4．4 分析結果
6．5 自動化分析TLS1．2 握手協議安全性
6．5．1 TLS1．2 握手協議
……
第三篇 基于計算模型自動化驗證安全協議Java實施
第四篇 基于計算模型自動化生成安全協議Java實施
第五篇 基于符號模型自動化生成安全協議Java實施
查看全部↓
新書資訊