本书系统地讲解了利用形式化方法对网络协议及系统进行安全性分析的原理、流程和典型工具，结合科研实例深入浅出地介绍了形式化安全方法的范畴、类型和使用技巧。全书内容密切围绕国家安全战略需求，紧跟时代发展，是对多年来该领域的科学研究与工程实践中基本原理与共性技术的归纳总结。本书分为三个单元，共8章。第一单元（第1～4章）主要介绍网络协议形式化安全分析方法的相关基础知识，包括绪论、离散数学基础知识、密码学基础知识、协议工程与软件工程基础知识等内容，明确了采用形式化方法对计算机系统中网络协议和软件的安全性进行分析的主要步骤，以及形式化安全方法发展的历史和趋势。第二单元（第5～7章）主要介绍现有的网络协议形式化安全分析方法，系统地讲解了相关方法在确保通信协议和软件实现的安全性方面的关键应用，包括基于演绎推理和自动机模型的形式化安全方法和基于进程演算的形式化方法。第三单元（第8章）主要介绍通信软件安全性的形式化验证实例，展示了形式化方法在实际安全应用中的具体实施和效果。 本书适合作为高等院校网络空间安全、信息安全专业或其他相关专业本科生和研究生的教材，也可供相关领域的科研人员参考。

第一单元 基础知识
第1章 绪论
1.1 形式化安全方法概述
1.2 通信安全中的形式化方法
1.3 软件安全中的形式化方法
1.3.1 软件安全的重要性与漏洞历史案例
1.3.2 软件漏洞的挑战与统计
1.3.3 软件安全技术与形式化方法的发展
本章小结
本章习题
第2章 离散数学基础知识
2.1 数理逻辑
2.1.1 命题逻辑与安全断言
2.1.2 命题逻辑的推理理论
2.1.3 一阶逻辑
2.1.4 时序逻辑与高阶逻辑
2.2 集合论
2.2.1 集合代数
2.2.2 二元关系与函数
2.3 代数结构
2.3.1 代数系统
2.3.2 群、环与格
2.4 图论
2.4.1 图的基本概念
2.4.2 树
本章小结
本章习题
第3章 密码学基础知识
3.1 密码基本理论与技术概述
3.1.1 密码学相关术语的定义
3.1.2 两类加密算法
3.2 对称密码
3.2.1 流密码
3.2.2 分组密码
3.3 公钥密码体制
3.3.1 公钥密码体制的基本概念
3.3.2 RSA密码机制
3.3.3 基于身份的密码机制
3.3.4 椭圆曲线密码机制
3.3.5 无证书密码机制
3.4 Hash函数
3.4.1 Hash函数用来提供认证的基本使用方式
3.4.2 Hash函数应满足的条件
3.4.3 第Ⅰ类生日攻击
3.4.4 第Ⅱ类生日攻击
3.5 数字签名
3.5.1 数字签名算法
3.5.2 椭圆曲线数字签名算法
3.5.3 代理签名算法
3.5.4 聚合签名算法
3.5.5 多重签名算法
本章小结
本章习题
第4章 协议工程与软件工程基础知识
4.1 协议工程
4.1.1 协议设计原理
4.1.2 协议安全
4.1.3 协议验证技术
4.2 软件工程
4.2.1 软件生命周期
4.2.2 软件安全
4.2.3 软件验证技术
本章小结
本章习题
第二单元 形式化安全分析方法
第5章 基于演绎推理的形式化安全方法
5.1 BAN逻辑
5.1.1 BAN逻辑的定义
5.1.2 形式化描述
5.1.3 形式化的协议验证目标
5.2 GNY逻辑
5.2.1 基本术语
5.2.2 推理规则
5.3 SVO逻辑
5.3.1 SVO逻辑的语法
5.3.2 SVO逻辑推理公理
5.3.3 SVO逻辑推理规则
5.4 演绎推理实例分析
5.4.1 使用BAN逻辑分析Kerberos协议
5.4.2 使用改进GNY逻辑分析Kerberos*协议
5.4.3 使用SVO逻辑分析改进Otway-Rees协议
本章小结
本章习题
第6章 基于自动机模型的形式化安全方法
6.1 FSM模型
6.1.1 图灵机与系统状态机
6.1.2 有限自动机的定义及分类
6.1.3 自动机模型的扩展
6.1.4 自动机模型的应用
6.2 Petri网模型
6.2.1 Petri网的原理
6.2.2 Petri网的扩展
6.2.3 Petri网的应用
6.3 标签转移系统（LTS）模型
6.3.1 标签转移系统的基本概念
6.3.2 标签转移系统的扩展
6.3.3 标签转移系统的应用
6.4 标准形式化语言
6.4.1 SDL语言
6.4.2 ESTELLE语言
6.5 自动化验证工具
6.5.1 SPIN
6.5.2 UPPAAL
6.6 实例分析与实验——用UPPAAL验证Prêt  Voter电子投票协议
本章小结
本章习题
第7章 基于进程演算的形式化方法
7.1 进程演算
7.1.1 进程代数体系
7.1.2 进程演算方法
7.2 CSP与CCS
7.2.1 CSP
7.2.2 CCS
7.3 标准语言——LOTOS
7.4 扩展模型
7.4.1 Security Pi Calculus
7.4.2 Applied Pi Calculus
7.4.3 Ambient Calculus
7.5 自动化工具
7.5.1 ProVerif
7.5.2 Tamarin
7.6 实例分析与实验
7.6.1 使用Tamarin验证Diffie Hellman协议
7.6.2 使用ProVerif分析5G-AKA协议
本章小结
本章习题
第三单元 形式化安全方法的综合应用
第8章 通信软件安全性的形式化验证实例
8.1 通信软件的形式化安全验证流程
8.1.1 通信软件设计的安全性验证流程
8.1.2 通信软件代码的安全性验证流程
8.2 通信软件形式化安全验证实例
8.2.1 分析对象
8.2.2 CHAP软件设计安全性验证
8.2.3 CHAP软件代码一致性验证
本章小结
参考文献