描述
开 本: 16开纸 张: 轻型纸包 装: 平装-胶订是否套装: 否国际标准书号ISBN: 9787121351952丛书名: 经典译丛·网络空间安全
本书涵盖从安全协议验证的基础理论到代码的实现，不仅为协议构建了牢固的数学形式化基础，进而精确地定义了协议的运行规范和安全属性，还设计了高效的验证算法。
第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
伴随着计算机技术和通信技术的发展，人们的生活方式也发生了极大的改变。移动终端的普及、大数据分析和各种人工智能应用悄悄地改变了人们的生活方式，信息安全问题也日益突出，上关国家安全，下系个人隐私保护。各种应用都依赖于底层的通信协议，为了确保协议的安全性，设计者往往利用密码要素增加协议的安全性。大量协议还被应用在关键性系统上，它们的安全分析和证明，乃至如何设计一个安全的协议，仍然是一件很困难的事情。
正如本书作者所述，安全工程师用高强度的密码算法设计出一个协议后，并不能保证通信协议的安全性。传统的安全分析依赖于设计者的经验和手工分析，这种做法在实践中已经被证明很难完全检测出系统的各种隐藏漏洞。协议运行环境的改变、安全假设的改变，都可能导致新的攻击。例如，伴随着移动计算的普及，一个设备上运行着多个不同的应用，每个应用对应着一个协议会话，多协议的并发运行将增加新的安全隐患。
本书涵盖了从安全协议验证的基础理论到代码的实现，不仅为协议构建了牢固的数学形式化基础，进而精确地定义了协议的运行规范和安全属性，还设计了高效的验证算法。作者不仅熟悉各种形式化理论，更难能可贵的是开发了多个开源的安全协议验证系统：基于标准模型的Scyther、提供机器证明的Scyther-Proof、高级的可交互式Tamarin。这些系统非常有利于协议的分析和学习，信息安全工程设计人员可以很方便地用验证系统检测协议的安全性能。
本书有一个配套的网页，提供了协议验证需要的工具、教学资料和参考文献。读者在阅读过程中可以下载相关工具并对协议实例进行验证分析，将有利于理解协议的运行和有关安全机制。验证工具提供了源码，非常方便高级研究者深入了解验证算法的细节。因此，本书非常适合作为信息安全和相关专业的教材，也可作为相关工程研究人员的参考书。
本书的翻译得到了国家自然科学基金(编号：61170282、61661019)和海南省自然科学基金(编号：614231)的资助和支持。特别感谢中国科学院软件研究所首席研究员、北京大学软件与微电子学院卿斯汉教授一直以来给予的关怀和帮助。全书由吴汉炜翻译，卿斯汉审校。由于时间仓促，不当之处在所难免，恳请读者批评指正。联系E-mail：[email protected]。
译 者
于海南大学东坡湖畔
前 言
大约十年前，Sjouke Mauw和Erik de Vink创建了荷兰艾恩德霍芬科技大学的计算机安全研究小组。凭借在形式化理论领域的深厚功底，他们开始关注安全协议的形式化建模与安全属性分析。他们发现，如果首先构建一个简洁的模型，然后用易于理解的操作语义概念描绘该模型，将非常有助于理解安全协议固有的复杂性。在研究开始后不久，Cas Cremers加入了研究小组，并把这个极具挑战性的领域作为他的博士研究课题。
这些年来，我们不仅在研究中深入探讨协议模型，还把它作为研究生教学中学习安全协议的理论基础。其间我们开发了Scyther 验证系统。该工具运行效率很高，能帮助我们快速证明协议的正确与否，并将验证理论应用到真实协议检测中。
本书的写作目的有三个。首先，简略介绍我们在安全协议理论研究上的成果。其次，本书可作为协议验证的基础教材。最后，当阐述完理论基础后，读者能将验证理论应用于实际分析。我们希望读者在阅读完本书后，能理解协议分析的内部机理和各种不同验证理论。
本书的出版得益于许多人的支持和帮助，没有他们的付出本书将无法面世。首先我们要特别向Erik de Vink表达我们的敬意。书中的许多概念、技术方案均由他提出，通过与他的热烈探讨，我们从中获益匪浅。
我们还要真挚地感谢Jos Baeten 和 David Basin，他们给了我们在这个领域连续几年研究和著书的机会。同时，还要感谢我们的编辑Ronan Nugent，在我们的写作过程中他给予了我们耐心的支持。
本书涉及的理论和陈述在这些年来经历了许多变化。我们要特别感谢为本书提出各种建设性意见的人士，他们是： David Basin、Ton van Deursen、Hugo Jonker、Barbara Kordy、Simon Meier、Matthijs Melissen、Marko Horvat、Sa?a Radomirovi?、Benedikt Schmidt和Christoph Sprenger。
最后，我们各自的家人在我们的写作过程中给我们提供了精神上的支持。没有他们，本书不可能面世。
Cas Cremers 于苏黎世
Sjouke Mauw 于卢森堡
评论
还没有评论。