安全协议操作语义与验证
批量上传，套装书可能不全，下单前咨询在线客服！ 正版书 ！！！
￥ 27.26 4.6折 ￥ 59 全新
库存6件
四川成都
认证卖家担保交易快速发货售后保障
作者（瑞士）Cas Cremers（卡斯?克雷默斯）, （卢森堡）Sjouke Mauw（肖克?毛弗）
出版社电子工业出版社
ISBN9787121351952
出版时间2018-11
装帧平装
开本16开
定价59元
货号25580701
上书时间2024-10-19
- 最新上架
商品详情
- 品相描述：全新
- 商品描述
-
前言
译 者 序
伴随着计算机技术和通信技术的发展，人们的生活方式也发生了极大的改变。移动终端的普及、大数据分析和各种人工智能应用悄悄地改变了人们的生活方式，信息安全问题也日益突出，上关国家安全，下系个人隐私保护。各种应用都依赖于底层的通信协议，为了确保协议的安全性，设计者往往利用密码要素增加协议的安全性。大量协议还被应用在关键性系统上，它们的安全分析和证明，乃至如何设计一个安全的协议，仍然是一件很困难的事情。
正如本书作者所述，安全工程师用高强度的密码算法设计出一个协议后，并不能保证通信协议的安全性。传统的安全分析依赖于设计者的经验和手工分析，这种做法在实践中已经被证明很难完全检测出系统的各种隐藏漏洞。协议运行环境的改变、安全假设的改变，都可能导致新的攻击。例如，伴随着移动计算的普及，一个设备上运行着多个不同的应用，每个应用对应着一个协议会话，多协议的并发运行将增加新的安全隐患。
本书涵盖了从安全协议验证的基础理论到代码的实现，不仅为协议构建了牢固的数学形式化基础，进而精确地定义了协议的运行规范和安全属性，还设计了高效的验证算法。作者不仅熟悉各种形式化理论，更难能可贵的是开发了多个开源的安全协议验证系统：基于标准模型的Scyther、提供机器证明的Scyther-Proof、高级的可交互式Tamarin。这些系统非常有利于协议的分析和学习，信息安全工程设计人员可以很方便地用验证系统检测协议的安全性能。
本书有一个配套的网页，提供了协议验证需要的工具、教学资料和参考文献。读者在阅读过程中可以下载相关工具并对协议实例进行验证分析，将有利于理解协议的运行和有关安全机制。验证工具提供了源码，非常方便高级研究者深入了解验证算法的细节。因此，本书非常适合作为信息安全和相关专业的教材，也可作为相关工程研究人员的参考书。
本书的翻译得到了国家自然科学基金(编号：61170282、61661019)和海南省自然科学基金(编号：614231)的资助和支持。特别感谢中国科学院软件研究所首席研究员、北京大学软件与微电子学院卿斯汉教授一直以来给予的关怀和帮助。全书由吴汉炜翻译，卿斯汉审校。由于时间仓促，不当之处在所难免，恳请读者批评指正。联系E-mail：wuhanwei@hainu.edu.cn。
译 者
于海南大学东坡湖畔
前 言
大约十年前，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 于卢森堡
导语摘要
安全协议作为信息安全的重要基础之一，其安全属性能否达到设计者的初始目标成为一个重要研究内容，关系到依赖于协议的上层应用系统的安全性。本书的内容主要涵盖两部分：用形式化的语义定义协议的执行规格和安全属性，精确表示安全协议的安全属性；综合运用各种形式化方法设计一个高效的验证算法，在可接受的时间内验证安全属性。本书还探讨了多协议安全分析，比较分析了各种验证理论和发展趋势。
作者简介
Cas Cremers 牛津大学信息安全领域正教授。2006 年获得荷兰艾恩德霍芬技术大学博士学位；2006 年至 2013 年，在瑞士苏黎世联邦理工学院任博士后和高级研究员；2013年开始在牛津大学任教，于2015 年成为正教授。近期他加入了位于德国的CISPA-Helmholtz中心。他擅长各种形式化理论和系统安全验证与加固，独立或与其他研究者一起开发了一系列协议验证系统，在国际上享有盛誉。Sjouke Mauw 博士，工作于卢森堡大学计算机科学与通信研究所。曾与人一起创建了荷兰埃因霍温理工大学的计算机安全研究小组，关注安全协议的形式化建模与安全属性分析。
Cas Cremers 牛津大学信息安全领域正教授。2006 年获得荷兰艾恩德霍芬科技大学博士学位；2006 年至 2013 年，在瑞士苏黎世联邦理工学院任博士后和高级研究员；2013年开始在牛津大学任教，于2015 年成为正教授。近期他加入了位于德国的CISPA-Helmholtz中心。他擅长各种形式化理论和系统安全验证与加固，独立或与其他研究者一起开发了一系列协议验证系统，在国际上享有盛誉。Sjouke Mauw 博士，工作于卢森堡大学计算机科学与通信研究所。曾与人合作创建了荷兰艾恩德霍芬科技大学的计算机安全研究小组，他关注安全协议的形式化建模与安全属性分析。
目录
目 录
第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 牛津大学信息安全领域正教授。2006 年获得荷兰艾恩德霍芬技术大学博士学位；2006 年至 2013 年，在瑞士苏黎世联邦理工学院任博士后和高级研究员；2013年开始在牛津大学任教，于2015 年成为正教授。近期他加入了位于德国的CISPA-Helmholtz中心。他擅长各种形式化理论和系统安全验证与加固，独立或与其他研究者一起开发了一系列协议验证系统，在国际上享有盛誉。Sjouke Mauw 博士，工作于卢森堡大学计算机科学与通信研究所。曾与人一起创建了荷兰埃因霍温理工大学的计算机安全研究小组，关注安全协议的形式化建模与安全属性分析。
Cas Cremers 牛津大学信息安全领域正教授。2006 年获得荷兰艾恩德霍芬科技大学博士学位；2006 年至 2013 年，在瑞士苏黎世联邦理工学院任博士后和高级研究员；2013年开始在牛津大学任教，于2015 年成为正教授。近期他加入了位于德国的CISPA-Helmholtz中心。他擅长各种形式化理论和系统安全验证与加固，独立或与其他研究者一起开发了一系列协议验证系统，在国际上享有盛誉。Sjouke Mauw 博士，工作于卢森堡大学计算机科学与通信研究所。曾与人合作创建了荷兰艾恩德霍芬科技大学的计算机安全研究小组，他关注安全协议的形式化建模与安全属性分析。
相关推荐
— 没有更多了 —
以下为对购买帮助不大的评价