扫一扫
关注中图网
官方微博
本类五星书更多>
-
>
全国计算机等级考试最新真考题库模拟考场及详解·二级MSOffice高级应用
-
>
决战行测5000题(言语理解与表达)
-
>
软件性能测试.分析与调优实践之路
-
>
第一行代码Android
-
>
C Primer Plus 第6版 中文版
-
>
深度学习
-
>
MATLAB计算机视觉与深度学习实战-赠在线交流卡和本书源码
安全协议形式化分析与验证 版权信息
- ISBN：9787030626332
- 条形码：9787030626332 ; 978-7-03-062633-2
- 装帧：平装-胶订
- 册数：暂无
- 重量：暂无
- 所属分类：>
安全协议形式化分析与验证 本书特色
本书内容主要包括以下部分：安全协议形式化分析背景及研究现状。介绍了安全协议及形式化方法基本概念，安全协议形式化分析研究发展历史和国内外研究现状。形式化方法基本理论。对模态逻辑、模型检测，定理证明三类形式化方法进行了详细阐述和对比分析，介绍了Murφ和Spin具有代表性的形式化分析工具。安全协议。介绍了安全协议的基本概念及分类，从安全协议受攻击类型角度提出安全协议形式化分析的必要性。
安全协议形式化分析与验证 内容简介
《安全协议形式化分析与验证》是作者多年从事安全协议形式化分析与验证相关科研工作的总结，主要对两种形式化方法做了归纳：基于SPIN工具的模型检测和事件逻辑。 《安全协议形式化分析与验证》主要内容如下：介绍了安全协议形式化分析的研究现状、主要技术流派，以及协议描述语言ProDL，阐述了基于算法知识逻辑的网络安全协议模型检测分析方法，用于显式地刻画入侵者模型能力；在网络安全协议验证模型生成系统中，采用偏序归约、语法重定序以及静态分析等优化策略，有效缓解模型检测过程中状态爆炸问题；对事件逻辑进行扩展，提出一系列规则，对安全协议进行形式化描述，无需显性刻画入侵者模型，只需分析协议动作之间的匹配顺序关系即可对协议的安全性进行证明。
安全协议形式化分析与验证 目录
目录
前言
第1章 绪论 1
1.1 安全协议形式化分析背景 1
1.2 安全协议形式化分析研究现状 3
参考文献 6
第2章 形式化方法基本理论 10
2.1 形式化方法概述 10
2.2 模态逻辑 11
2.2.1 BAN逻辑 11
2.2.2 BAN类逻辑 14
2.2.3 Kailar逻辑 15
2.3 模型检测 15
2.3.1 FDR 16
2.3.2 NRL协议分析器 19
2.3.3 Murφ 21
2.3.4 SPIN 23
2.4 定理证明 26
2.4.1 Paulson归纳法 27
2.4.2 串空间模型 28
2.4.3 Spi演算证明方法 29
2.4.4 PCL证明方法 30
2.4.5 事件逻辑证明方法 33
2.5 比较与分析 35
参考文献 36
第3章 安全协议 39
3.1 安全协议概念 39
3.2 安全协议分类 40
3.2.1 ISO/IEC 11770-2密钥建立机制6协议 40
3.2.2 NSSK协议 41
3.2.3 Kerberos认证协议 42
3.2.4 ISO/IEC 9798-3协议 44
3.2.5 NSPK协议 44
3.3 协议安全属性 45
3.4 协议安全构建方法 46
3.4.1 Hash函数 48
3.4.2 随机数 49
3.4.3 时间戳 50
3.5 协议攻击者模型及其攻击类型 51
3.5.1 Dolev-Yao攻击者模型 52
3.5.2 攻击类型 53
参考文献 53
第4章 基于模型检测的安全协议分析 55
4.1 安全协议形式化表示 55
4.1.1 原子消息(基本约定) 55
4.1.2 消息 55
4.1.3 动作 56
4.1.4 协议 57
4.1.5 迹 57
4.2 消息生成规则 58
4.3 基于算法知识逻辑的协议形式化分析 61
4.3.1 多智体系统 62
4.3.2 算法知识逻辑 62
4.3.3 算法知识逻辑分析协议 64
4.4 时态逻辑 69
4.4.1 Kripke结构 70
4.4.2 CTL*、CTL和LTL 70
4.4.3 并发系统性质描述 72
4.4.4 实例 73
4.5 形式化分析流程 74
4.5.1 形式化建模 75
4.5.2 协议安全性质刻画 79
4.5.3 形式化验证 79
4.6 验证模型优化策略 79
4.6.1 静态分析 79
4.6.2 语法重定序 84
4.6.3 偏序归约 84
4.6.4 优化策略对比 87
4.7 与其他方法对比 88
4.7.1 与认证逻辑对比 89
4.7.2 与FDR对比 91
4.7.3 与Murφ对比 93
4.7.4 与NRL协议分析器对比 95
4.7.5 与Athena对比 97
4.7.6 与Isabelle对比 100
4.7.7 与BRUTUS对比 101
参考文献 103
第5章 网络安全协议验证模型生成系统 108
5.1 系统概述 108
5.1.1 系统简介 108
5.1.2 系统功能 110
5.2 系统设计与实现 112
5.2.1 整体设计 112
5.2.2 模块设计 112
5.2.3 协议描述语言ProDL 124
5.2.4 Needham-Schroeder公开密钥协议分析与验证 130
5.2.5 BAN-Yahalom三方对称密钥认证协议分析与验证 132
5.2.6 CMP1可信第三方电子商务协议分析与验证 133
参考文献 135
第6章 基于事件逻辑的安全协议形式化分析 137
6.1 事件系统 137
6.1.1 符号说明 137
6.1.2 消息自动机 138
6.1.3 语法语义 139
6.1.4 不可猜测的原子 140
6.1.5 事件结构 140
6.1.6 事件类 142
6.2 事件逻辑公理、推论及性质 143
6.2.1 事件逻辑公理 143
6.2.2 事件逻辑推论及性质 146
6.3 事件逻辑形式化描述协议 147
6.4 基于事件逻辑的安全协议证明 150
6.4.1 推理规则 150
6.4.2 两方安全协议证明流程 151
6.4.3 三方安全协议证明流程 153
6.5 与其他典型证明方法对比 154
6.5.1 PCL 154
6.5.2 BAN类逻辑 155
6.5.3 串空间理论 155
参考文献 156
第7章 总结与展望 158
7.1 研究成果总结 158
7.2 下一步研究工作 159
前言
第1章 绪论 1
1.1 安全协议形式化分析背景 1
1.2 安全协议形式化分析研究现状 3
参考文献 6
第2章 形式化方法基本理论 10
2.1 形式化方法概述 10
2.2 模态逻辑 11
2.2.1 BAN逻辑 11
2.2.2 BAN类逻辑 14
2.2.3 Kailar逻辑 15
2.3 模型检测 15
2.3.1 FDR 16
2.3.2 NRL协议分析器 19
2.3.3 Murφ 21
2.3.4 SPIN 23
2.4 定理证明 26
2.4.1 Paulson归纳法 27
2.4.2 串空间模型 28
2.4.3 Spi演算证明方法 29
2.4.4 PCL证明方法 30
2.4.5 事件逻辑证明方法 33
2.5 比较与分析 35
参考文献 36
第3章 安全协议 39
3.1 安全协议概念 39
3.2 安全协议分类 40
3.2.1 ISO/IEC 11770-2密钥建立机制6协议 40
3.2.2 NSSK协议 41
3.2.3 Kerberos认证协议 42
3.2.4 ISO/IEC 9798-3协议 44
3.2.5 NSPK协议 44
3.3 协议安全属性 45
3.4 协议安全构建方法 46
3.4.1 Hash函数 48
3.4.2 随机数 49
3.4.3 时间戳 50
3.5 协议攻击者模型及其攻击类型 51
3.5.1 Dolev-Yao攻击者模型 52
3.5.2 攻击类型 53
参考文献 53
第4章 基于模型检测的安全协议分析 55
4.1 安全协议形式化表示 55
4.1.1 原子消息(基本约定) 55
4.1.2 消息 55
4.1.3 动作 56
4.1.4 协议 57
4.1.5 迹 57
4.2 消息生成规则 58
4.3 基于算法知识逻辑的协议形式化分析 61
4.3.1 多智体系统 62
4.3.2 算法知识逻辑 62
4.3.3 算法知识逻辑分析协议 64
4.4 时态逻辑 69
4.4.1 Kripke结构 70
4.4.2 CTL*、CTL和LTL 70
4.4.3 并发系统性质描述 72
4.4.4 实例 73
4.5 形式化分析流程 74
4.5.1 形式化建模 75
4.5.2 协议安全性质刻画 79
4.5.3 形式化验证 79
4.6 验证模型优化策略 79
4.6.1 静态分析 79
4.6.2 语法重定序 84
4.6.3 偏序归约 84
4.6.4 优化策略对比 87
4.7 与其他方法对比 88
4.7.1 与认证逻辑对比 89
4.7.2 与FDR对比 91
4.7.3 与Murφ对比 93
4.7.4 与NRL协议分析器对比 95
4.7.5 与Athena对比 97
4.7.6 与Isabelle对比 100
4.7.7 与BRUTUS对比 101
参考文献 103
第5章 网络安全协议验证模型生成系统 108
5.1 系统概述 108
5.1.1 系统简介 108
5.1.2 系统功能 110
5.2 系统设计与实现 112
5.2.1 整体设计 112
5.2.2 模块设计 112
5.2.3 协议描述语言ProDL 124
5.2.4 Needham-Schroeder公开密钥协议分析与验证 130
5.2.5 BAN-Yahalom三方对称密钥认证协议分析与验证 132
5.2.6 CMP1可信第三方电子商务协议分析与验证 133
参考文献 135
第6章 基于事件逻辑的安全协议形式化分析 137
6.1 事件系统 137
6.1.1 符号说明 137
6.1.2 消息自动机 138
6.1.3 语法语义 139
6.1.4 不可猜测的原子 140
6.1.5 事件结构 140
6.1.6 事件类 142
6.2 事件逻辑公理、推论及性质 143
6.2.1 事件逻辑公理 143
6.2.2 事件逻辑推论及性质 146
6.3 事件逻辑形式化描述协议 147
6.4 基于事件逻辑的安全协议证明 150
6.4.1 推理规则 150
6.4.2 两方安全协议证明流程 151
6.4.3 三方安全协议证明流程 153
6.5 与其他典型证明方法对比 154
6.5.1 PCL 154
6.5.2 BAN类逻辑 155
6.5.3 串空间理论 155
参考文献 156
第7章 总结与展望 158
7.1 研究成果总结 158
7.2 下一步研究工作 159
展开全部
书友推荐
- >
李白与唐代文化
李白与唐代文化
¥9.9¥29.8 - >
二体千字文
二体千字文
¥16.0¥40.0 - >
有舍有得是人生
有舍有得是人生
¥19.4¥45.0 - >
史学评论
史学评论
¥13.9¥42.0 - >
山海经
山海经
¥20.4¥68.0 - >
新文学天穹两巨星--鲁迅与胡适/红烛学术丛书(红烛学术丛书)
新文学天穹两巨星--鲁迅与胡适/红烛学术丛书(红烛学术丛书)
¥11.0¥23.0 - >
我与地坛
我与地坛
¥16.8¥28.0 - >
伯纳黛特,你要去哪(2021新版)
伯纳黛特,你要去哪(2021新版)
¥15.9¥49.8
本类畅销
-
数学之美
¥48.3¥69 -
浪潮之巅-下册-第二版
¥22.1¥45 -
挑战程序设计竞赛(第2版)
¥55.3¥79 -
算法竞赛入门经典-(第2版)
¥34.9¥49.8 -
2022图书×抽奖盲袋
¥9.9¥25 -
2023读书月阅读盲盒——天黑，闭眼，刀谁？
¥42.3¥158
