密碼協議實現的邏輯安全分析與設計

本書主要探討密碼協議實現（密碼協議程序源代碼）
時的邏輯安全性，並以密碼協議實現時的安全性為前提條件，設計了新的方案。
本書引入了邏輯推理與規則的安全證明，在分析方面，討論了密碼協議實現時的軌跡安全、
快速判斷密碼協議實現時導致的不安全原因、基於內容安全的密碼協議代碼實現模型分析和密碼協議實現時的側信道安全分析。
在設計方面，討論了非簽名認證的密鑰協商協議設計和基於協議底層實現安全的密鑰協商協議。
所有的方法都通過源代碼（C語言和Socket通信編程）進行實驗分析，實驗結果符合預期要求。
本書可作為計算機科學與技術、網絡空間安全、數學與應用數學等信息安全專業本科生、研究生的學術性指導教材，
也可供高等院校從事網絡空間安全研究的學者以及其他領域對信息安全感興趣的愛好者作為參考資料之用。

第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 從控制流圖到狀態圖