网络安全协议的形式化分析 / 新一代信息技术（网络空间安全）系列丛书
￥42.00定价
作者： 付玉龙
出版时间：2025-04
出版社：西安电子科技大学出版社
- 西安电子科技大学出版社
- 9787560675176
- 1-1
- 549934
- 16开
- 2025-04
- 自动化技术、计算机技术
- 本科
目录
目录
第一单元 基 础 知 识
第1章 绪论2
1.1 形式化安全方法概述2
1.2 通信安全中的形式化方法4
1.3 软件安全中的形式化方法6
1.3.1 软件安全的重要性与漏洞历史案例6
1.3.2 软件漏洞的挑战与统计6
1.3.3 软件安全技术与形式化方法的发展7
本章小结8
本章习题8
第2章 离散数学基础知识9
2.1 数理逻辑9
2.1.1 命题逻辑与安全断言9
2.1.2 命题逻辑的推理理论11
2.1.3 一阶逻辑12
2.1.4 时序逻辑与高阶逻辑15
2.2 集合论15
2.2.1 集合代数16
2.2.2 二元关系与函数17
2.3 代数结构19
2.3.1 代数系统20
2.3.2 群、 环与格20
2.4 图论22
2.4.1 图的基本概念22
2.4.2 树30
本章小结38
本章习题39
第3章 密码学基础知识40
3.1 密码基本理论与技术概述40
3.1.1 密码学相关术语的定义41
3.1.2 两类加密算法41
3.2 对称密码43
3.2.1 流密码43
3.2.2 分组密码46
3.3 公钥密码体制61
3.3.1 公钥密码体制的基本概念62
3.3.2 RSA密码机制65
3.3.3 基于身份的密码机制68
3.3.4 椭圆曲线密码机制73
3.3.5 无证书密码机制77
3.4 Hash函数82
3.4.1 Hash函数用来提供认证的基本使用方式82
3.4.2 Hash函数应满足的条件84
3.4.3 第Ⅰ类生日攻击85
3.4.4 第Ⅱ类生日攻击85
3.5 数字签名85
3.5.1 数字签名算法86
3.5.2 椭圆曲线数字签名算法89
3.5.3 代理签名算法91
3.5.4 聚合签名算法94
3.5.5 多重签名算法95
本章小结96
本章习题97
第4章 协议工程与软件工程基础知识 98
4.1 协议工程98
4.1.1 协议设计原理99
4.1.2 协议安全100
4.1.3 协议验证技术101
4.2 软件工程104
4.2.1 软件生命周期105
4.2.2 软件安全109
4.2.3 软件验证技术110
本章小结124
本章习题124
第二单元 形式化安全分析方法
第5章 基于演绎推理的形式化安全方法126
5.1 BAN逻辑126
5.1.1 BAN逻辑的定义126
5.1.2 形式化描述127
5.1.3 形式化的协议验证目标131
5.2 GNY逻辑131
5.2.1 基本术语131
5.2.2 推理规则132
5.3 SVO逻辑133
5.3.1 SVO逻辑的语法134
5.3.2 SVO逻辑推理公理134
5.3.3 SVO逻辑推理规则136
5.4 演绎推理实例分析137
5.4.1 使用BAN逻辑分析Kerberos协议138
5.4.2 使用改进GNY逻辑分析Kerberos*协议141
5.4.3 使用SVO逻辑分析改进Otway-Rees协议143
本章小结145
本章习题146
第6章 基于自动机模型的形式化安全方法147
6.1 FSM模型147
6.1.1 图灵机与系统状态机148
6.1.2 有限自动机的定义及分类151
6.1.3 自动机模型的扩展157
6.1.4 自动机模型的应用158
6.2 Petri网模型160
6.2.1 Petri网的原理160
6.2.2 Petri网的扩展163
6.2.3 Petri网的应用164
6.3 标签转移系统（LTS）模型164
6.3.1 标签转移系统的基本概念164
6.3.2 标签转移系统的扩展167
6.3.3 标签转移系统的应用168
6.4 标准形式化语言171
6.4.1 SDL语言171
6.4.2 ESTELLE语言173
6.5 自动化验证工具174
6.5.1 SPIN174
6.5.2 UPPAAL179
6.6 实例分析与实验——用UPPAAL验证Prêt Voter电子投票协议181
本章小结185
本章习题186
第7章 基于进程演算的形式化方法187
7.1 进程演算187
7.1.1 进程代数体系188
7.1.2 进程演算方法189
7.2 CSP与CCS192
7.2.1 CSP192
7.2.2 CCS196
7.3 标准语言——LOTOS199
7.4 扩展模型201
7.4.1 Security Pi Calculus202
7.4.2 Applied Pi Calculus206
7.4.3 Ambient Calculus211
7.5 自动化工具213
7.5.1 ProVerif214
7.5.2 Tamarin216
7.6 实例分析与实验217
7.6.1 使用Tamarin验证Diffie Hellman协议217
7.6.2 使用ProVerif分析5G-AKA协议219
本章小结223
本章习题223
第三单元 形式化安全方法的综合应用
第8章 通信软件安全性的形式化验证实例226
8.1 通信软件的形式化安全验证流程226
8.1.1 通信软件设计的安全性验证流程226
8.1.2 通信软件代码的安全性验证流程227
8.2 通信软件形式化安全验证实例228
8.2.1 分析对象228
8.2.2 CHAP软件设计安全性验证229
8.2.3 CHAP软件代码一致性验证231
本章小结237
参考文献238
第一单元 基 础 知 识
第1章 绪论2
1.1 形式化安全方法概述2
1.2 通信安全中的形式化方法4
1.3 软件安全中的形式化方法6
1.3.1 软件安全的重要性与漏洞历史案例6
1.3.2 软件漏洞的挑战与统计6
1.3.3 软件安全技术与形式化方法的发展7
本章小结8
本章习题8
第2章 离散数学基础知识9
2.1 数理逻辑9
2.1.1 命题逻辑与安全断言9
2.1.2 命题逻辑的推理理论11
2.1.3 一阶逻辑12
2.1.4 时序逻辑与高阶逻辑15
2.2 集合论15
2.2.1 集合代数16
2.2.2 二元关系与函数17
2.3 代数结构19
2.3.1 代数系统20
2.3.2 群、 环与格20
2.4 图论22
2.4.1 图的基本概念22
2.4.2 树30
本章小结38
本章习题39
第3章 密码学基础知识40
3.1 密码基本理论与技术概述40
3.1.1 密码学相关术语的定义41
3.1.2 两类加密算法41
3.2 对称密码43
3.2.1 流密码43
3.2.2 分组密码46
3.3 公钥密码体制61
3.3.1 公钥密码体制的基本概念62
3.3.2 RSA密码机制65
3.3.3 基于身份的密码机制68
3.3.4 椭圆曲线密码机制73
3.3.5 无证书密码机制77
3.4 Hash函数82
3.4.1 Hash函数用来提供认证的基本使用方式82
3.4.2 Hash函数应满足的条件84
3.4.3 第Ⅰ类生日攻击85
3.4.4 第Ⅱ类生日攻击85
3.5 数字签名85
3.5.1 数字签名算法86
3.5.2 椭圆曲线数字签名算法89
3.5.3 代理签名算法91
3.5.4 聚合签名算法94
3.5.5 多重签名算法95
本章小结96
本章习题97
第4章 协议工程与软件工程基础知识 98
4.1 协议工程98
4.1.1 协议设计原理99
4.1.2 协议安全100
4.1.3 协议验证技术101
4.2 软件工程104
4.2.1 软件生命周期105
4.2.2 软件安全109
4.2.3 软件验证技术110
本章小结124
本章习题124
第二单元 形式化安全分析方法
第5章 基于演绎推理的形式化安全方法126
5.1 BAN逻辑126
5.1.1 BAN逻辑的定义126
5.1.2 形式化描述127
5.1.3 形式化的协议验证目标131
5.2 GNY逻辑131
5.2.1 基本术语131
5.2.2 推理规则132
5.3 SVO逻辑133
5.3.1 SVO逻辑的语法134
5.3.2 SVO逻辑推理公理134
5.3.3 SVO逻辑推理规则136
5.4 演绎推理实例分析137
5.4.1 使用BAN逻辑分析Kerberos协议138
5.4.2 使用改进GNY逻辑分析Kerberos*协议141
5.4.3 使用SVO逻辑分析改进Otway-Rees协议143
本章小结145
本章习题146
第6章 基于自动机模型的形式化安全方法147
6.1 FSM模型147
6.1.1 图灵机与系统状态机148
6.1.2 有限自动机的定义及分类151
6.1.3 自动机模型的扩展157
6.1.4 自动机模型的应用158
6.2 Petri网模型160
6.2.1 Petri网的原理160
6.2.2 Petri网的扩展163
6.2.3 Petri网的应用164
6.3 标签转移系统（LTS）模型164
6.3.1 标签转移系统的基本概念164
6.3.2 标签转移系统的扩展167
6.3.3 标签转移系统的应用168
6.4 标准形式化语言171
6.4.1 SDL语言171
6.4.2 ESTELLE语言173
6.5 自动化验证工具174
6.5.1 SPIN174
6.5.2 UPPAAL179
6.6 实例分析与实验——用UPPAAL验证Prêt Voter电子投票协议181
本章小结185
本章习题186
第7章 基于进程演算的形式化方法187
7.1 进程演算187
7.1.1 进程代数体系188
7.1.2 进程演算方法189
7.2 CSP与CCS192
7.2.1 CSP192
7.2.2 CCS196
7.3 标准语言——LOTOS199
7.4 扩展模型201
7.4.1 Security Pi Calculus202
7.4.2 Applied Pi Calculus206
7.4.3 Ambient Calculus211
7.5 自动化工具213
7.5.1 ProVerif214
7.5.2 Tamarin216
7.6 实例分析与实验217
7.6.1 使用Tamarin验证Diffie Hellman协议217
7.6.2 使用ProVerif分析5G-AKA协议219
本章小结223
本章习题223
第三单元 形式化安全方法的综合应用
第8章 通信软件安全性的形式化验证实例226
8.1 通信软件的形式化安全验证流程226
8.1.1 通信软件设计的安全性验证流程226
8.1.2 通信软件代码的安全性验证流程227
8.2 通信软件形式化安全验证实例228
8.2.1 分析对象228
8.2.2 CHAP软件设计安全性验证229
8.2.3 CHAP软件代码一致性验证231
本章小结237
参考文献238
