本书主要探讨密码协议实现 (密码协议程序源代码) 时的逻辑安全性, 引入了逻辑推理与规则的安全证明, 在分析方面讨论了密码协议实现时的轨迹安全、快速判断密码协议实现时导致不安全原因、基于内容安全的密码协议代码实现模型分析和密码协议实现时的侧信道安全分析。在设计方面, 本书讨论了非签名认证的密钥协商协议设计和基于协议底层实现安全的密钥协商协议。所有的逻辑实现方案都通过源代码 (C语言和Socket通信编程) 进行实验分析, 实验结果符合预期要求。李延斌, 男, 武汉大学网络空间安全学院信息安全专业博士学位, 2013年至今从事密码学及应用、侧信道攻击与防护、密码芯片及嵌入式安全等方面的研究工作。发表包括IEEE TIFS、TCAD等在内的SCI/EI论文10余篇。主持或参与多项密码学应用及信息系统安全的国家基金项目和省部级项目。