安全协议理论与方法 (2008 年度畅销榜NO.7117 )

本书是《信息安全国家重点实验室信息安全丛书》之一。书中系统地介绍了当前计算机网络安全协议的理论和方法，主要内容包括安全协议的基本概念、缺陷以及可能受到的攻击类型，基于推理结构性方法，基于攻击结构性方法，基于证明结构性方法，安全协议分析的形式化接口，安全协议设计的形式化方法，Kerberos协议，IPSec协议，SSL协议，X．509以及SET协议。\r\n\r\n 本书可作为高等院校计算机、通信、信息安全等专业的教学参考书，也可供从事相关专业的教学、科研和工程技术人员参考。\r\n
\r\n

第1章 引论 \r\n\r\n 1. 1 密码体制 \r\n\r\n 1. 1. 1 基本原理 \r\n\r\n 1. 1. 2 对称密钥密码体制 \r\n\r\n 1. 1. 3 公钥密码体制 \r\n\r\n 1. 2 数字签名 \r\n\r\n 1. 2. 1 数字签名(Digital Signature)技术 \r\n\r\n 1. 2. 2 数字签名技术与加密技术的结合 \r\n\r\n 1. 2. 3 几种新型的数字签名方案 \r\n\r\n 1. 3 Hash函数 \r\n\r\n 1. 4 密钥管理与分配 \r\n\r\n 1. 4. 1 密钥的管理 \r\n\r\n 1. 4. 2 密钥的分配 \r\n\r\n 1. 4. 3 公钥证明书 \r\n\r\n 1. 5 PKI公钥基础设施 \r\n\r\n 第2章 安全协议 \r\n\r\n 2. 1 安全协议概述 \r\n\r\n 2. 1. 1 安全协议的概念 \r\n\r\n 2. 1. 2 安全协议系统模型 \r\n\r\n 2. 1. 3 安全协议的安全性质及实现 \r\n\r\n 2. 2 安全协议的缺陷 \r\n\r\n 2. 2. 1 协议设计准则 \r\n\r\n 2. 2. 2 安全协议缺陷分类 \r\n\r\n 2. 2. 3 消息重放攻击及对策 \r\n\r\n 2. 3 安全协议及其受到的攻击实例 \r\n\r\n 2. 3. 1 无可信第三方参与的对称密钥协议 \r\n\r\n 2. 3. 2 有可信第三方参与的对称密钥协议 \r\n\r\n 2. 3. 3 无可信第三方参与的公钥协议 \r\n\r\n 2. 3. 4 有可信第三方参与的公钥协议 \r\n\r\n 2. 3. 5 其他相关协议 \r\n\r\n 2. 4 安全协议的形式化分析 \r\n\r\n 2. 4. 1 安全协议形式化分析概述 \r\n\r\n 2. 4. 2 安全协议形式化分析的历史与现状 \r\n\r\n 2. 4. 3 有关问题 \r\n\r\n 小结 \r\n\r\n 第3章 基于推理结构性方法 \r\n\r\n 3. 1 BAN逻辑 \r\n\r\n 3. 1. 1 BAN逻辑的基本框架 \r\n\r\n 3. 1. 2 应用实例 \r\n\r\n 3. 1. 3 BAN逻辑的缺陷 \r\n\r\n 3. 1. 4 BAN逻辑的设计准则 \r\n\r\n 3. 2 GNY逻辑 \r\n\r\n 3. 2. 1 GNY逻辑的简单计算模型 \r\n\r\n 3. 2. 2 GNY逻辑的语法和语义 \r\n\r\n 3. 2. 3 GNY逻辑的推理规则 \r\n\r\n 3. 2. 4 GNY逻辑对协议的分析 \r\n\r\n 3. 3 AT逻辑 \r\n\r\n 3. 3. 1 AT逻辑的基本符号 \r\n\r\n 3. 3. 2 AT逻辑的推理规则和公理 \r\n\r\n 3. 3. 3 AT逻辑的计算模型 \r\n\r\n 3. 3. 4 AT逻辑的语义 \r\n\r\n 3. 4 SVO逻辑 \r\n\r\n 3. 4. 1 SVO逻辑的基本结构 \r\n\r\n 3. 4. 2 SVO逻辑的推理规则及公理 \r\n\r\n 3. 4. 3 SVO逻辑语义 \r\n\r\n 3. 4. 4 SVO逻辑的应用实例 \r\n\r\n 3. 5 Kailar逻辑 \r\n\r\n 3. 5. 1 Kailar逻辑的基本架构 \r\n\r\n 3. 5. 2 Kailar逻辑的应用实例 \r\n\r\n 3. 5. 3 Kailar逻辑的缺陷 \r\n\r\n 3. 6 CS逻辑 \r\n\r\n 3. 6. 1 逻辑框架 \r\n\r\n 3. 6. 2 CS逻辑的扩展 \r\n\r\n 3. 6. 3 实例分析 \r\n\r\n 3. 7 KG逻辑 \r\n\r\n 3. 7. 1 基本标记与假设 \r\n\r\n 3. 7. 2 推理规则 \r\n\r\n 3. 7. 3 实例分析 \r\n\r\n 3. 8 Nonmonotomic逻辑 \r\n\r\n 3. 8. 1 基本符号和逻辑框架 \r\n\r\n 3. 8. 2 推理规则 \r\n\r\n 3. 8. 3 协议分析流程 \r\n\r\n 小结 \r\n\r\n 第4章 基于攻击结构性方法 \r\n\r\n 4. 1 一般目的的验证语言 \r\n\r\n 4. 1. 1 一阶谓词逻辑扩展 \r\n\r\n 4. 1. 2 Mur∮验证系统 \r\n\r\n 4. 1. 3 CSP与安全性质 \r\n\r\n 4. 1. 4 MOdel Checking \r\n\r\n 4. 2 单一代数理论模型 \r\n\r\n 4. 2. 1 Dolev-Yao模型 \r\n\r\n 4. 2. 2 Merritt模型 \r\n\r\n 4. 2. 3 Meadows模型 \r\n\r\n 4. 2. 4 Woo-Lam模型 \r\n\r\n 4. 3 特别目的的专家系统 \r\n\r\n 4. 3. 1 Interrogator \r\n\r\n 4. 3. 2 NRL协议分析器 \r\n\r\n 4. 3. 3 基于规则系统 \r\n\r\n 小结 \r\n\r\n 第5章 基于证明结构性方法 \r\n\r\n 5. 1 human—readable证明法 \r\n\r\n 5. 1. 1 主体知识及操作 \r\n\r\n 5. 1. 2 协议形式化分析实例 \r\n\r\n 5. 1. 3 并行多重会话 \r\n\r\n 5. 2 Paulson归纳法 \r\n\r\n 5. 2. 1 归纳法概述 \r\n\r\n 5. 2. 2 归纳法的自动化理论 \r\n\r\n 5. 2. 3 归纳法对一个递归协议的分析 \r\n\r\n 5. 3 Schneider秩函数 \r\n\r\n 5. 3. 1 秩函数的定义 \r\n\r\n 5. 3. 2 主要定理 \r\n\r\n 5. 3. 3 实例分析 \r\n\r\n 5. 3. 4 新版秩函数 \r\n\r\n 5. 4 strand space \r\n\r\n 5. 4. 1 理论框架 \r\n\r\n 5. 4. 2 攻击者 \r\n\r\n 5. 4. 3 协议的正确性 \r\n\r\n 5. 4. 4 NSL协议分析 \r\n\r\n 5. 4. 5 ideal \r\n\r\n 5. 4. 6 对Otway-Rees协议的分析 \r\n\r\n 5. 5 Attacks限定法 \r\n\r\n 5. 5. 1 认证协议模型 \r\n\r\n 5. 5. 2 限定 \r\n\r\n 5. 5. 3 约简定理 \r\n\r\n 5. 6 Rewriting逼近法 \r\n\r\n 5. 6. 1 预备知识 \r\n\r\n 5. 6. 2 逼近技术 \r\n\r\n 5. 6. 3 对NS公钥协议和攻击者的编码 \r\n\r\n 5. 6. 4 逼近和验证 \r\n\r\n 5. 7 Maude分析法 \r\n\r\n 5. 7. 1 Maude的面向对象的说明 \r\n\r\n 5. 7. 2 NS公钥协议的说明与执行 \r\n\r\n 5. 7. 3 攻击者和一个攻击 \r\n\r\n 5. 7. 4 宽度优先搜索策略 \r\n\r\n 5. 8 invariant技术 \r\n\r\n 5. 8. 1 基本概念 \r\n\r\n 5. 8. 2 描述攻击者不可知术语集合属性的不变式 \r\n\r\n 5. 8. 3 描述攻击者可知消息集合属性的不变式 \r\n\r\n 小结 \r\n\r\n 第6章 安全协议分析的形式化语言 \r\n\r\n 6. 1 安全协议分析语言：CPAL \r\n\r\n 6. 1. 1 CPAL行为的含义 \r\n\r\n 6. 1. 2 CPAL的语法 \r\n\r\n 6. 1. 3 CPAL的形式化语义 \r\n\r\n 6. 1. 4 CPAL协议评估系统 \r\n\r\n 6. 1. 5 使用CPAL评估系统对协议进行验证 \r\n\r\n 6. 2 安全协议简单接口说明语言——ISLSLAAPA \r\n\r\n 6. 2. 1 ISL定义 \r\n\r\n 6. 2. 2 AAPA的输出 \r\n\r\n 6. 2. 3 与基于攻击结构性工具的比较 \r\n\r\n 6. 3 安全协议通用说明语言——CAPSL \r\n\r\n 6. 3. 1 CAPSL集成环境 \r\n\r\n 6. 3. 2 CAPSL \r\n\r\n 6. 3. 3 分析工具接口格式 \r\n\r\n 6. 3. 4 翻译器算法 \r\n\r\n 6. 3. 5 安全协议的分析 \r\n\r\n 6. 4 安全协议分析编译器Casper \r\n\r\n 6. 4. 1 Casper的语法 \r\n\r\n 6. 4. 2 Casper的实施 \r\n\r\n 6. 4. 3 实例分析：大嘴青蛙(WMF)协议 \r\n\r\n 6. 4. 4 与CAPSL的比较 \r\n\r\n 6. 5 安全协议的积分——spi积分 \r\n\r\n 6. 5. 1 使用限制性信道的协议 \r\n\r\n 6. 5. 2 使用密码体制的协议 \r\n\r\n 6. 5. 3 spi积分的形式化语义 \r\n\r\n 小结 \r\n\r\n 第7章 安全协议设计的形式化方法 \r\n\r\n 7. 1 Heintze&Tygar：模型及其构成 \r\n\r\n 7. 1. 1 模型和安全性 \r\n\r\n 7. 1. 2 协议和非记时模型 \r\n\r\n 7. 1. 3 协议的组合 \r\n\r\n 7. 2 GongSLSynersion：fail-stop协议 \r\n\r\n 7. 2. 1 fail-stop协议及其分析 \r\n\r\n 7. 2. 2 方法的应用 \r\n\r\n 7. 2. 3 fail-safe协议 \r\n\r\n 7. 2. 4 使用因果一致性概念的形式化 \r\n\r\n 7. 3 Buttyan&Staaman简单逻辑 \r\n\r\n 7. 3. 1 模型 \r\n\r\n 7. 3. 2 简单逻辑 \r\n\r\n 7. 3. 3 分析和修正Woo&Lam认证协议 \r\n\r\n 7. 4 Rudolph抽象模型 \r\n\r\n 7. 4. 1 原理 \r\n\r\n 7. 4. 2 抽象协议的APA模型 \r\n\r\n 7. 4. 3 协议级联 \r\n\r\n 小结 \r\n\r\n 第8章 Kerberos \r\n\r\n 8. 1 Kerberos协议概况 \r\n\r\n 8. 1. 1 cross—realm操作 \r\n\r\n 8. 1. 2 通信主体的选择 \r\n\r\n 8. 1. 3 授权 \r\n\r\n 8. 1. 4 环境假设 \r\n\r\n 8. 1. 5 术语 \r\n\r\n 8. 2 票据标志使用与请求 \r\n\r\n 8. 3 消息交换 \r\n\r\n 8. 3. 1 认证服务交换 \r\n\r\n 8. 3. 2 客户／服务器认证交换 \r\n\r\n 8. 3. 3 TGS交换 \r\n\r\n 8. 3. 4 KRB—SAFE交换 \r\n\r\n 8. 4 ULTRIX操作系统上Kerberos的实现 \r\n\r\n 第9章 IPSet协议 \r\n\r\n 9. 1 IPSec体系结构 \r\n\r\n 9. 2 安全联盟 \r\n\r\n 9. 3 IPSec的安全协议 \r\n\r\n 9. 3. 1 IPSec的模式 \r\n\r\n 9. 3. 2 封装安全载荷(ESP) \r\n\r\n 9. 3. 3 认证头(AH) \r\n\r\n 9. 4 IPSec的应用 \r\n\r\n 第10章 SSLV3. 0 \r\n\r\n 10. 1 SSLV3. 0概况 \r\n\r\n 10. 1. 1 SSLV3. 0的特点 \r\n\r\n 10. 1. 2 SSLV3. 0的结构 \r\n\r\n 10. 1. 3 SSLV3. 0的加密属性 \r\n\r\n 10. 1. 4 SSLV3. 0的通信主体 \r\n\r\n 10. 2 SSLV3. 0中的状态 \r\n\r\n 10. 2. 1 会话状态和连接状态 \r\n\r\n 10. 2. 2 预备状态和当前操作状态 \r\n\r\n 10. 3 记录层协议 \r\n\r\n 10. 4 ChangeCipherSpec协议 \r\n\r\n 10. 5 Alerr协议 \r\n\r\n 10. 5. 1 close—notify消息 \r\n\r\n 10. 5. 2 error alerts消息 \r\n\r\n 10. 6 握手协议层 \r\n\r\n 第11章 X. 509 \r\n\r\n 11. 1 X. 509 v3证书概述 \r\n\r\n 11. 1. 1 证书路径和信任 \r\n\r\n 11. 1. 2 撤消 \r\n\r\n 11. 1. 3 操作协议／管理协议 \r\n\r\n 11. 2 证书及其扩展 \r\n\r\n 11. 2. 1 基本证书域 \r\n\r\n 11. 2. 2 标准证书扩展 \r\n\r\n 11. 3 CRL及其扩展 \r\n\r\n 11. 3. 1 CRL域 \r\n\r\n 11. 3. 2 CRL扩展 \r\n\r\n 11. 3. 3 CRL输入项扩展 \r\n\r\n 11. 4 证明路径的检验 \r\n\r\n 11. 4. 1 基本路径检验 \r\n\r\n 11. 4. 2 扩展路径检验 \r\n\r\n 11. 5 算法支持 \r\n\r\n 11. 5. 1 单向Hash函数 \r\n\r\n 11. 5. 2 签名算法 \r\n\r\n 11. 5. 3 公钥加密算法 \r\n\r\n 第12章 SET协议 \r\n\r\n 12. 1 背景及商业要求 \r\n\r\n 12. 2 系统设计 \r\n\r\n 12. 2. 1 SET系统结构 \r\n\r\n 12. 2. 2 安全服务及证书 \r\n\r\n 12. 2. 3 技术要求 \r\n\r\n 12. 3 证书管理结构 \r\n\r\n 12. 4 证书请求协议 \r\n\r\n 12. 4. 1 主协议 \r\n\r\n 12. 4. 2 持卡人证书发起请求／响应处理 \r\n\r\n 12. 4. 3 持卡人注册表单请求／响应处理 \r\n\r\n 12. 4. 4 商家／支付网关证书发起处理 \r\n\r\n 12. 4. 5 证书请求和生成处理 \r\n\r\n 12. 4. 6 证书质询及状态处理 \r\n\r\n 12. 5 证书撤消 \r\n\r\n 12. 5. 1 持卡人证书的撤消 \r\n\r\n 12. 5. 2 商家证书撤消 \r\n\r\n 12. 5. 3 支付网关证书撤消 \r\n\r\n 12. 5. 4 CA崩溃恢复 \r\n\r\n 12. 6 SET私有扩展 \r\n\r\n 12. 6. 1 HashedRootKey私有扩展 \r\n\r\n 12. 6. 2 CertificateType私有扩展 \r\n\r\n 12. 6. 3 MerchantData私有扩展 \r\n\r\n 12. 6. 4 CardCertRequired私有扩展 \r\n\r\n 12. 6. 5 Tunneling私有扩展 \r\n\r\n 12. 6. 6 SETExtensions私有扩展 \r\n\r\n 参考文献 \r\n
\r\n

人类的进步得益于科学研究的突破. 生产力的发展和社会的进步.

计算机. 通信. 半导体科学技术的突破, 形成了巨大的新型生产力. 数字化的生存方式席卷全球. 农业革命. 工业革命. 信息革命成为人类历史生产力发展的三座丰碑. 古老的中华大地, 也正在以信息化带动工业化的国策下焕发着青春. 电子政务. 电子商务等各种信息化应用之花, 如雨后春笋, 在华夏沃土上竞相开放, 炎黄子孙们, 在经历了几百年的苦难历程后, 在国家崛起中又迎来了一个运用勤劳和智慧富国强民的新契机.

科学规律的掌握, 非一朝一夕之功. 治水. 训火. 利用核能都曾经经历了多么漫长的时日. 不掌握好科学技术造福人类的一面, 就会不经意地释放出它危害人类的一面.

生产力的发展, 为社会创造出许多新的使用价值. 但是, 工具的不完善, 会限制这些使用价值的真正发挥. 信息化工具也和农业革命. 工业革命中人们曾创造的许多工具一样, 由于人类认识真理和实践真理的客观局限性, 存在许多不完善的地方, 从而形成信息系统的漏洞, 造成系统的脆弱性, 在人们驾御技能不足的情况下, 损害着人们自身的利益.

世界未到大同时, 社会上和国际间存在着竞争. 斗争. 战争和犯罪. 传统社会存在的不文明. 暴力, 在信息空间也同样存在. 在这个空间频频发生的有些人利用系统存在的脆弱性, 运用其“暴智”来散布计算机病毒, 制造拒绝服务的事端, 甚至侵入他人的系统, 盗窃资源. 资产, 以达到其贪婪的目的. 人类运用智慧开拓的信息疆土正在被这些暴行蚕食破坏着.

随着信息化的发展, 信息安全成为全社会的需求, 信息安全保障成为国际社会关注的焦点. 因为信息安全不但关系国家的政治安全. 经济安全. 军事安全. 社会稳定, 也关系到社会中每一个人的数字化生存的质量.

信息革命给人类带来的高效率和高效益是否真正实现, 取决于信息安全是否得以保障. 什么是信息安全?怎样才能保障信息安全?这些问题都是严肃的科学和技术问题. 面对人机结合, 非线性. 智能化的复杂信息巨系统, 我们还有许多科学技术问题需要认真的研究. 我们不能在研究尚处肤浅的时候, 就盲目乐观地向世人宣称, 我们拥有了全面的解决方案, 我们也不能因为面对各种麻烦, 就灰头鼠脸, 自暴自弃, 我们需要的是具有革命的乐观主义精神, 坚忍不拔的奋勇攀登科学技术高峰的坚定信念.

人是有能力认识真理的, 今天对信息安全的认识, 就经历了一个从保密到保护, 又发展到保障的趋近真理的发展过程. 因为信息安全的问题不仅仅是因为技术原因引起的, 它涉及到人. 社会和技术, 因此, 仅仅靠技术是不能有效地实施信息安全保障的. 从社会学的观点来看, 只有依靠有信息安全觉悟和技能的人及科学有效

的管理来实施综合的技术保障手段, 才能取得良好的效果.

为了推动我国信息化发展的进程, 信息安全国家重点实验室组织编写了《信息安全国家重点实验室信息安全丛书》. 在本丛书的编写过程中, 我们既注重学术水平, 又注意其实用价值. 本丛书从信息安全保障体系, 操作系统安全, 数据库安全, 网络安全, 无线网络安全, 网络攻击, 密码技术, PKI技术, 信息隐藏, 安全协议, 安全事件应急响应, 量子密码通信等多个角度, 分析和总结信息安全的科学问题以及信息安全保障的理论与技术, 因此, 这套丛书有较大的适用范围. 我们将努力把国内外信息安全的最新研究成果写进书中, 以使一些读者阅读本丛书后在理论. 方法. 技术上有新的启发和收获, 从而切实解决工作中的实际问题.

本丛书的组织方式是开放式的, 今后将根据学科发展陆续组织出版信息安全领域的优秀图书.

信息安全只能是相对而言, 它是动态发展的. 任何人都不能宣称自己终极了对信息安全的认识. 让我们一起努力, 不断地深化自己的研究, 借鉴国外先进的科学技术, 结合国情, 与时俱进地推出信息安全保障的新理论. 新办法和新手段, 用我们的智慧保卫我们的信息疆土, 使我们的信息家园尽量祥和安宁.

限于作者的水平, 本丛书难免存在不足之处, 敬请读者批评指正.

《信息安全国家重点实验室信息安全丛书》编委会

2003年7月

网络安全是目前人们关注的一个热点. 在一个分布式的互联网网络环境中, 人们通过安全协议来具体实现安全共享网络资源的需求. 已有的安全协议往往被证实并不如它们的设计者所期望的那样安全, 复杂的网络环境使得攻击者可利用安全协议自身的缺陷来实施各种各样的攻击, 从而达到破坏网络安全的目的, 因此, 安全协议的安全性成为网络安全的关键. 安全性的达成需从两方面着手, 一是安全协议的安全性是否满足形式化的分析, 二是对安全协议进行形式化的设计. 本书对现在国内外最新的安全协议形式化分析与设计方法进行了比较详细的论述, 建立了完整而系统的安全协议研究理论, 并介绍了当前的最为实用的几个安全协议, 包括Kerberos协议. IPSec协议. SSL协议. X. 509以及SET协议的实现方法.

全书共12章. 第1章介绍了安全协议所涉及的一些基础密码学知识, 包括密码体制. 数学签名. Hash函数. 密钥管理与分配以及公钥证书和基础设施. 第2章主要介绍了安全协议的概念. 缺陷与可能受到的攻击类型. 认证协议及其所受攻击实例, 以及安全协议形式化分析的研究现状与面临的新问题. 第3章到第6章介绍了现有的一些安全协议形式化分析方法, 包括基于推理结构性方法, 基于攻击结构性方法, 基于证明结构性方法, 以及安全协议分析的形式化接口, 第7章介绍了安全协议设计的形式化方法. 第8章到第12章介绍了五个安全协议的实现方法和工作原理, 包括Kerberos协议. IPSec协议. SSL协议. X. 509以及SET协议.

本书是作者在长期从事理论研究和科研实践的基础上编写的, 我们汲取了大量国内外现有文献的精华, 对内容做了精心的安排以适应不同层次和不同专业的读者的需求. 书的最后附有相关的参考文献, 提供了与本书有关的资料, 供有兴趣的读者参考.

作者

2003年5月