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

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