●第1章 緒論
1.1 引言
1.2 關鍵技術
1.3 本書結構介紹
參考文獻
第2章 密碼協議實現安全的研究現狀
2.1 代碼模型提取安全驗證分析
2.1.1 C語言模型提取分析
2.1.2 Java語言模型提取分析
2.1.3 F#語言模型提取分析
2.2 代碼自動生成安全驗證分析
2.2.1 基於編譯器代碼自動生成分析
2.2.2 基於Java語言代碼自動生成分析
2.3 基於操作語義安全驗證分析
2.4 密碼協議精化安全驗證分析
2.4.1 精化檢測工具協議分析
2.4.2 程序精化分析
2.4.3 信息流精化分析
2.5 本章小結
參考文獻
第3章 非簽名認證的密鑰協商協議設計
3.1 新協議涉及的群同態基礎知識
3.1.1 群同態的基本定義
3.1.2 群同態的基本定理
3.2 整數乘法同態二叉樹的構造與分析
3.3 整數乘法同態二叉樹的基本遍歷與性質
3.4 整數乘法同態二叉樹的密鑰協商協議
3.4.1 構造一棵葉子結點為素數的整數乘法同態二叉樹
3.4.2 整數乘法同態二叉樹密鑰協商協議具體步驟
3.5 協議安全分析
3.5.1 一般安全性分析
3.5.2 隨機預言模型（Random Oracle Model）的可證明安全分析
3.6 新協議結構的安全分析
3.7 新協議性能比較與實驗分析
3.7.1 新協議的二叉樹存儲與遍歷
3.7.2 新協議實現的實驗
3.7.3 參數n對網絡通信的影響
3.8 本章小結
參考文獻
第4章 通過密碼協議在代碼級上實現時的軌跡行為是否異常來評估其安全性
4.1 相關研究工作
4.2 知識準備
4.2.1 標號遷移繫統與強模擬
4.2.2 程序的精化
4.2.3 密碼協議源代碼的程序精化
4.3 建立模型
4.3.1 密碼協議的符號化描述
4.3.2 密碼協議源代碼精化
4.3.3 程序控制流圖
4.3.4 從控制流圖到狀態圖
4.3.5 密碼協議實現的軌跡
4.4 密碼協議實現的安全分析
4.4.1 函數返回值的操作語義
4.4.2 非理想軌跡與理想軌跡
4.5 針對Needham-Schroeder協議與Diffie-Hellman協議及它們的改進協議在理想與攻擊環境下的實驗
4.5.1 新方法實現的步驟
4.5.2 Needham-Schroeder協議及其改進協議實現的實驗
4.5.3 Diffie-Hellman協議及其改進協議實現的實驗
4.5.4 密碼協議實現的實驗分析
4.6 本章小結
參考文獻
第5章 快速判斷密碼協議在代碼級上實現時導致的不安全原因
5.1 相關研究工作
5.2 知識準備
5.2.1 標號遷移繫統
5.2.2 密碼協議實現操作語義
5.2.3 密碼協議實現規範
5.3 新模型的建立
5.3.1 函數返回值字典
5.3.2 函數返回值序列
5.3.3 密碼協議代碼實現安全分析
5.4 針對經典密碼協議的實驗與分析
5.4.1 NSL協議代碼實現的符號化規範
5.4.2 NSL協議部分源代碼標注
5.4.3 NSL協議代碼實現的安全分析
5.4.4 新模型與原來模型比較
5.5 本章小結
參考文獻
第6章 針對代碼底層彙編語言實現跳轉設計新的密鑰協商協議
6.1 知識準備
6.1.1 程序運行時寄存器的分配情況
6.1.2 程序調用（CALL）與返回（RET）操作情況
6.1.3 內存溢出造成漏洞攻擊情況
6.2 改進的密鑰協商協議
6.2.1 基礎知識
6.2.2 改進的密鑰協商協議設計
6.3 改進的密鑰協商協議安全分析
6.3.1 基於密碼理論的安全分析
6.3.2 基於串空間的改進的密鑰協商協議實現的安全分析
6.4 基於RET改進的密鑰協商協議實驗
6.4.1 修改RET配件鏈
6.4.2 密鑰協商協議實驗
6.4.3 實驗結果與性能分析
6.5 本章小結
參考文獻
第7章 基於內容安全的密碼協議代碼實現行為安全
7.1 相關研究工作
7.2 基礎知識
7.2.1 霍恩子句邏輯
7.2.2 密碼協議規範
7.3 新模型的建立與分析
7.3.1 密碼協議的操作語義
7.3.2 建立密碼協議行為安全的分析模型
7.4 基於經典密碼協議的新分析方法實驗
7.4.1 具體的實現步驟
7.4.2 模擬實驗
7.5 安全與性能分析
7.5.1 NSL協議描述
7.5.2 NSL協議代碼實現的安全分析
7.5.3 行為安全分析
7.5.4 新模型與現有分析模型比較
7.6 本章小結
參考文獻
第8章 密碼協議的軟件實現安全分析
8.1 軟件實現的物理層安全
8.1.1 側信道攻擊
8.1.2 密碼協議軟件實現的物理層安全
8.2 密碼防護方案的實現安全
8.2.1 掩碼方案安全性
8.2.2 軟件實現安全性分析
8.2.3 針對實際環境中軟件實現的安全性分析實驗
8.2.4 防護策略
8.3 本章小結
參考文獻
第9章 總結與未來展望
9.1 總結
9.2 未來展望
參考文獻

本書主要探討密碼協議實現（密碼協議程序源代碼）時的邏輯安全性，引入了邏輯推理與規則的安全證明，在分析方面討論了密碼協議實現時的軌跡安全、快速判斷密碼協議實現時導致不安全原因、基於內容安全的密碼協議代碼實現模型分析和密碼協議實現時的側信道安全分析。在設計方面，本書討論了非簽名認證的密鑰協商協議設計和基於協議底層實現安全的密鑰協商協議。所有的邏輯實現方案都通過源代碼（C語言和Socket通信編程）進行實驗分析，實驗結果符合預期要求。李延斌，男，武漢大學網絡空間安全學院信息安全專業博士學位，2013年至今從事密碼學及應用、側信道攻擊與防護、密碼芯片及嵌入式安全等方面的研究工作。發表包括IEEE TIFS、TCAD等在內的SCIEI論文10餘篇。主持或參與多項密碼學應用及信息繫統安全的國家基金項目和省部級項目。