网络安全协议的形式化分析 - 新一代信息技术(网络空间安全)系列丛书 - 中国高校教材图书网
|
书名： |
网络安全协议的形式化分析
新一代信息技术(网络空间安全)系列丛书
|
| ISBN： | 9787560675176 |
条码： | 9787560675176 |
| 作者： |
付玉龙
相关图书
|
装订： | 0 |
| 印次： | 1-1 |
开本： | 16开 |
| 定价： |
￥42.00
折扣价：￥39.90
折扣：0.95
节省了2.1元
|
字数： |
248千字
|
| 出版社： |
西安电子科技大学出版社 |
页数： |
365页
|
| 发行编号： | |
每包册数： |
|
| 出版日期： |
2025-04-25 |
|
|
| 内容简介： |
本书系统地讲解了利用形式化方法对网络协议及系统进行安全性分析的原理、流程和典型工具，结合科研实例深入浅出地介绍了形式化安全方法的范畴、类型和使用技巧。全书内容密切围绕国家安全战略需求，紧跟时代发展，是对多年来该领域的科学研究与工程实践中基本原理与共性技术的归纳总结。本书分为三个单元，共8章。第一单元（第1～4章）主要介绍网络协议形式化安全分析方法的相关基础知识，包括绪论、 离散数学基础知识、 密码学基础知识、 协议工程与软件工程基础知识等内容，明确了采用形式化方法对计算机系统中网络协议和软件的安全性进行分析的主要步骤，以及形式化安全方法发展的历史和趋势。第二单元（第5～7章）主要介绍现有的网络协议形式化安全分析方法，系统地讲解了相关方法在确保通信协议和软件实现的安全性方面的关键应用，包括基于演绎推理和自动机模型的形式化安全方法和基于进程演算的形式化方法。第三单元（第8章）主要介绍通信软件安全性的形式化验证实例，展示了形式化方法在实际安全应用中的具体实施和效果。
本书适合作为高等院校网络空间安全、信息安全专业或其他相关专业本科生和研究生的教材，也可供相关领域的科研人员参考。
|
| 作者简介： |
|
|
| 章节目录： |
目录
第一单元 基 础 知 识
第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
|
| 精彩片段： |
|
|
| 书 评： |
|
|
| 其 它： |
|
|
|
中国大学出版社协会 |
首页 |
宏观指导 |
出版社天地 |
图书代办站 |
教材图书信息 |
教材图书评论 |
在线订购 |
教材征订
