西电出版社

网络安全协议的形式化分析收藏

作者：付玉龙曹进李晖蔺如嫣

策划编辑：李惠萍

书代号：781800

I S B N：978-7-5606-7517-6

出版日期：2025-04印刷日期：2025-04

业务分类：本科;

纸书价格：￥35.7元原价：￥42元

（教授相关专业课程的教师可申请教材类样书1~2本，非教材类图书不提供样书）

相关资源

(如需下载资源请在电脑浏览器上浏览图书)

内容简介

本书系统地讲解了利用形式化方法对网络系统进行安全性分析的原理、流程和典型工具，结合科研实例深入浅出地介绍了形式化安全方法的范畴、类型和使用技巧。全书内容密切围绕国家安全战略需求，紧跟时代发展，是对多年...

前言

密码学的发展为人们提供了保护隐私和保障通信安全的有力工具，然而，密码技术本身并不足以完全确保信息安全。如何正确、合理地使用密码，如何确保密码在应用中的有效性和安全性，这需要更深层次的理解和更高的智慧...

目录

第一单元基础知识

1.1 形式化安全方法概述2

1.2 通信安全中的形式化方法4

1.3 软件安全中的形式化方法6

1.3.1 软件安全的重要性与漏洞历史案例6

1.3.2 软件漏洞的挑战与统计6

1.3.3 软件安全技术与形式化方法的发展7

第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.1 图的基本概念22

第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

第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.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.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

序

编辑推荐

查看全部> >

本书系统地讲解了利用形式化方法对网络系统进行安全性分析的原理、流程和典型工具，结合科研实例深入浅出地介绍了形式化安全方法的范畴、类型和使用技巧。全书内容密切围绕国家安全战略需求，紧跟时代发展，是对多年...