-
>
决战行测5000题(言语理解与表达)
-
>
软件性能测试.分析与调优实践之路
-
>
第一行代码Android
-
>
深度学习
-
>
Unreal Engine 4蓝图完全学习教程
-
>
深入理解计算机系统-原书第3版
-
>
Word/Excel PPT 2013办公应用从入门到精通-(附赠1DVD.含语音视频教学+办公模板+PDF电子书)
经典译丛·网络空间安全安全协议操作语义与验证/(瑞士)CAS CREMERS 版权信息
- ISBN:9787121351952
- 条形码:9787121351952 ; 978-7-121-35195-2
- 装帧:一般胶版纸
- 册数:暂无
- 重量:暂无
- 所属分类:>
经典译丛·网络空间安全安全协议操作语义与验证/(瑞士)CAS CREMERS 本书特色
适读人群 :本书可作为高等院校信息安全、计算机和通信等专业的教学参考书,也可供从事相关专业的教学、科研和工程技术人员参考。 安全工程师用高强度的密码算法设计出一个协议后,并不能保证通信协议的安全性。传统的安全分析依赖于设计者的经验和手工分析,这种做法在实践中已经被证明很难完全检测出系统的各种隐藏漏洞。协议运行环境的改变、安全假设的改变,都可能导致新的攻击。 本书涵盖从安全协议验证的基础理论到代码的实现,不仅为协议构建了牢固的数学形式化基础,进而精确地定义了协议的运行规范和安全属性,还设计了高效的验证算法。
经典译丛·网络空间安全安全协议操作语义与验证/(瑞士)CAS CREMERS 内容简介
安全协议作为信息安全的重要基础之一,其安全属性能否达到设计者的初始目标成为一个重要研究内容,关系到依赖于协议的上层应用系统的安全性。本书的内容主要涵盖两部分:用形式化的语义定义协议的执行规格和安全属性,准确表示安全协议的安全属性;综合运用各种形式化方法设计一个高效的验证算法,在可接受的时间内验证安全属性。本书还探讨了多协议安全分析,比较分析了各种验证理论和发展趋势。
经典译丛·网络空间安全安全协议操作语义与验证/(瑞士)CAS CREMERS 目录
目 录
第1章 背景介绍 1
1.1 历史背景 1
1.2 基于黑盒的安全协议分析 3
1.3 目的与方法 5
1.4 概要 5
1.4.1 协议分析模型 6
1.4.2 模型的应用 6
第2章 预备知识 7
2.1 集合与关系 7
2.2 巴科斯范式 8
2.3 符号变迁系统 8
第3章 操作语义 10
3.1 问题域分析 10
3.2 安全协议规范 13
3.2.1 角色项 14
3.2.2 协议规范 16
3.2.3 事件次序 18
3.3 协议执行描绘 20
3.3.1 回合 20
3.3.2 匹配 21
3.3.3 回合事件 23
3.3.4 威胁模型 24
3.4 操作语义 25
3.5 协议规范实例 27
3.6 思考题 28
第4章 安全属性 29
4.1 安全断言事件属性 29
4.2 机密性 30
4.3 认证 32
4.3.1 存活性 32
4.3.2 同步一致性 35
4.3.3 非单射同步一致性 37
4.3.4 单射同步一致性 38
4.3.5 消息一致性 39
4.4 认证继承关系 41
4.5 对NS协议的攻击和改进 44
4.6 总结 49
4.7 思考题 50
第5章 验证 52
5.1 模式 52
5.2 验证算法 58
5.2.1 良构模式 59
5.2.2 可达模式 59
5.2.3 空模式和冗余模式 60
5.2.4 算法概述 61
5.2.5 模式精炼 62
5.3 搜索空间遍历实例 66
5.4 使用模式精炼验证安全属性 70
5.5 启发式算法和参数选择 71
5.5.1 启发式算法 71
5.5.2 选择一个合适的回合数 74
5.5.3 性能 75
5.6 验证单射性 76
5.6.1 单射同步一致性 76
5.6.2 LOOP循环属性 79
5.6.3 模型假设 82
5.7 更多Scyther分析系统的特性 82
5.8 思考题 84
第6章 多协议攻击 85
6.1 多协议攻击概述 86
6.2 实验 86
6.3 测试结果 87
6.3.1 严格类型匹配:无类型缺陷 89
6.3.2 简单类型匹配:基本类型缺陷 90
6.3.3 无类型匹配:所有类型缺陷 90
6.3.4 攻击例子 90
6.4 攻击场景 92
6.4.1 协议更新 92
6.4.2 歧义性身份验证 94
6.5 预防多协议攻击 96
6.6 总结 97
6.7 思考题 97
第7章 基于NSL扩展的多方认证 98
7.1 一个多方身份认证协议 98
7.2 安全分析 101
7.2.1 初步检测 101
7.2.2 正确性证明 102
7.2.3 角色 的随机数机密性 105
7.2.4 初始化角色 的非单射同步一致性 106
7.2.5 非初始化角色 的随机数机密性 107
7.2.6 非初始化角色 的非单射同步一致性 107
7.2.7 所有角色的单射同步一致性 108
7.2.8 类型缺陷攻击 108
7.2.9 消息*小化 108
7.3 模式变体 109
7.4 弱多方认证协议 111
7.5 思考题 112
第8章 历史背景和进阶阅读 114
8.1 历史背景 114
8.1.1 模型 114
8.1.2 早期分析工具 114
8.1.3 逻辑 114
8.1.4 验证工具 115
8.1.5 多协议攻击 117
8.1.6 复杂度分析 117
8.1.7 符号化模型和计算模型之间的差异 117
8.1.8 消除安全分析和代码实现之间的差异 118
8.2 可选方法 119
8.2.1 建模框架 119
8.2.2 安全属性 120
8.2.3 验证工具 122
参考文献 125
经典译丛·网络空间安全安全协议操作语义与验证/(瑞士)CAS CREMERS 作者简介
Cas Cremers 牛津大学信息安全领域正教授。2006 年获得荷兰艾恩德霍芬技术大学博士学位;2006 年至 2013 年,在瑞士苏黎世联邦理工学院任博士后和高级研究员;2013年开始在牛津大学任教,于2015 年成为正教授。近期他加入了位于德国的CISPA-Helmholtz中心。他擅长各种形式化理论和系统安全验证与加固,独立或与其他研究者一起开发了一系列协议验证系统,在国际上享有盛誉。Sjouke Mauw 博士,工作于卢森堡大学计算机科学与通信研究所。曾与人一起创建了荷兰埃因霍温理工大学的计算机安全研究小组,关注安全协议的形式化建模与安全属性分析。Cas Cremers 牛津大学信息安全领域正教授。2006 年获得荷兰艾恩德霍芬科技大学博士学位;2006 年至 2013 年,在瑞士苏黎世联邦理工学院任博士后和高级研究员;2013年开始在牛津大学任教,于2015 年成为正教授。近期他加入了位于德国的CISPA-Helmholtz中心。他擅长各种形式化理论和系统安全验证与加固,独立或与其他研究者一起开发了一系列协议验证系统,在国际上享有盛誉。Sjouke Mauw 博士,工作于卢森堡大学计算机科学与通信研究所。曾与人合作创建了荷兰艾恩德霍芬科技大学的计算机安全研究小组,他关注安全协议的形式化建模与安全属性分析。
- >
小考拉的故事-套装共3册
小考拉的故事-套装共3册
¥36.7¥68.0 - >
二体千字文
二体千字文
¥21.6¥40.0 - >
月亮与六便士
月亮与六便士
¥18.1¥42.0 - >
名家带你读鲁迅:朝花夕拾
名家带你读鲁迅:朝花夕拾
¥10.5¥21.0 - >
龙榆生:词曲概论/大家小书
龙榆生:词曲概论/大家小书
¥7.7¥24.0 - >
月亮虎
月亮虎
¥20.2¥48.0 - >
中国历史的瞬间
中国历史的瞬间
¥16.7¥38.0 - >
自卑与超越
自卑与超越
¥13.5¥39.8
-
基于近邻思想和同步模型的聚类算法
¥44.1¥59 -
深度学习
¥92.4¥168 -
微信背后的产品观
¥62.6¥88 -
NGINX经典教程
¥89.9¥119.8 -
图解TCP/IP(第6版)
¥56.9¥79.8 -
物联网动态服务的协同感知与调控优化
¥51.4¥72
认罪认罚从宽制度中的刑事辩护问题研究
¥49.0¥68.0传统村落社区旅游产权保障机制研究
¥37.4¥68.0