本书主要探讨密码协议实现（密码协议程序源代码）时的逻辑安全性，并以密码协议实现时的安全性为前提条件，设计了新的方案。本书引入了逻辑推理与规则的安全证明，在分析方面，讨论了密码协议实现时的轨迹安全、快速判断密码协议实现时导致的不安全原因、基于内容安全的密码协议代码实现模型分析和密码协议实现时的侧信道安全分析。在设计方面，讨论了非签名认证的密钥协商协议设计和基于协议底层实现安全的密钥协商协议。所有的方法都通过源代码（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 从控制流图到状态图
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 未来展望
参考文献