Security Protocol

第1章 引言
1.1 信息系统与信息系统安全
1.2 信息系统的攻击与防御
1.2.1 被动窃听与主动攻击
1.2.2 信息对抗的历史回顾
1.2.3 攻击目标与攻击分类
1.2.4 入侵检测技术
1.3 数学基础
1.3.1 数论基础
1.3.2 代数基础
1.3.3 计算复杂性理论基础
1.4 本书的取材、组织与安排
第2章 安全协议的密码学基础
2.1 密码学的基本概念
2.2 古典密码学
2.2.1 换位密码
2.2.2 代替密码
2.2.3 转轮密码机
2.3 分组密码
2.3.1 分组乘积密码
2.3.2 数据加密标准
2.3.3 IDEA密码体制
2.3.4 先进加密标准和Rijndael密码算法
2.3.5 分组密码的工作模式
2.4 公开密钥密码
2.4.1 公开密钥密码的基本概念
2.4.2 MH背包体制
2.4.3 RSA体制
2.4.4 Rabin体制
2.5 数字签名
2.5.1 数字签名的基本概念
2.5.2 RSA数字签名
2.5.3 数字签名标准
2.6 散列函数
2.6.1 散列函数的基本概念
2.6.2 安全散列标准
2.7 总结
习题
第3章 认证协议
3.1 经典认证协议
3.1.1 NSSK协议
3.1.2 NSPK协议
3.1.3 Otway-Rees协议
3.1.4 Yahalom协议
3.1.5 Andrew安全RPC协议
3.1.6 “大嘴青蛙”协议
3.2 关于认证协议攻击的讨论
3.2.1 Dolev-Yao模型
3.2.2 攻击者的知识和能力
3.2.3 重放攻击
3.3 针对经典认证协议的攻击
3.3.1 针对NSSK协议的攻击
3.3.2 针对NSPK协议的攻击
3.3.3 针对Otway-Rees协议的“类型缺陷”型攻击
3.3.4 针对Yahalom协议的攻击
3.3.5 针对Andrew安全RPC协议的攻击
3.3.6 针对“大嘴青蛙”协议的攻击
3.4 其他重要的认证协议
3.4.1 Kerberos协议
3.4.2 Helsinki协议
3.4.3 Woo-Lam单向认证协议
3.5 认证协议攻击的其他实例
3.5.1 攻击A(O)协议的3种新方法
3.5.2 攻击NSSK协议的一种新方法
3.5.3 攻击Otway-Rees协议的两种新方法
3.6 有关认证协议的进一步讨论
3.6.1 认证协议设计与分析的困难性
3.6.2 认证协议的分类
3.6.3 认证协议的设计原则
3.7 总结
习题
第4章 BAN类逻辑
4.1 BAN逻辑
4.1.1 BAN逻辑构件的语法和语义
4.1.2 BAN逻辑的推理规则
4.1.3 BAN逻辑的推理步骤
4.2 应用BAN逻辑分析NSSK协议
4.2.1 应用BAN逻辑分析原始NSSK协议
4.2.2 应用BAN逻辑分析改进的NSSK协议
4.3 应用BAN逻辑分析Otway-Rees协议
4.4 应用BAN逻辑分析Yahalom协议
4.5 BAN类逻辑
4.5.1 Nessett对BAN逻辑的批评
4.5.2 BAN类逻辑
4.6 SVO逻辑
4.6.1 SVO逻辑的特点
4.6.2 SVO逻辑的语法
4.6.3 SVO逻辑的语义
4.6.4 应用SVO逻辑分析A(O)协议
4.6.5 应用SVO逻辑分析改进的A(O)协议
4.7 关于认证协议和BAN类逻辑的讨论
4.8 总结
习题
第5章 非否认协议与安全电子商务协议
5.1 非否认协议
5.1.1 非否认协议的基本概念
5.1.2 基本符号
5.1.3 一个非否认协议的例子
5.1.4 应用SVO逻辑分析非否认协议
5.2 安全电子商务协议的基本概念
5.2.1 安全电子商务协议的基本需求
5.2.2 安全电子商务协议的基本结构
5.2.3 安全电子商务协议的分类
5.3 典型的安全电子商务协议
5.3.1 SET协议
5.3.2 IBS协议
5.3.3 ISI协议
5.3.4 NetBill协议
5.3.5 First Virtual协议
5.3.6 iKP协议
5.3.7 在线数字货币协议
5.3.8 离线数字货币协议
5.3.9 Zhou-Gollmann协议
5.4 iKPI协议
5.4.1 iKPI协议概要
5.4.2 iKPI协议提出的背景
5.4.3 iKPI协议的系统模型与安全要求
5.4.4 iKPI协议的基本流程
5.4.5 iKPI协议的安全性分析
5.4.6 iKPI协议的实现
5.5 安全电子商务协议中的可信第三方
5.5.1 三类TTP协议
5.5.2 TTP的角色
5.5.3 一个简单的例子
5.6 三类可信第三方协议及其分析
5.6.1 Inline TTP协议的例子——Coffey-Saidha协议
5.6.2 Online TTP协议的例子——CMP1协议
5.6.3 Offline TTP协议的例子——Asokan-Shoup-Waidner协议
5.7 总结
习题
第6章 安全电子商务协议的形式化分析
6.1 Kailar逻辑
6.1.1 Kailar逻辑的构件
6.1.2 Kailar逻辑的推理规则
6.1.3 关于Kailar逻辑的进一步说明
6.1.4 Kailar逻辑的分析步骤
6.2 应用Kailar逻辑分析安全电子商务协议
6.2.1 CMP1协议的安全性分析
6.2.2 Zhou-Gollmann协议的安全性分析
6.2.3 IBS协议的安全性分析
6.3 Kailar逻辑的缺陷及其改进
6.3.1 Kailar逻辑的缺陷分析
6.3.2 新方法概述
6.3.3 基本符号
6.3.4 概念和定义
6.3.5 推理规则
6.3.6 协议分析的步骤
6.4 新形式化方法的分析实例
6.4.1 ISI协议的分析
6.4.2 CMP1协议的分析
6.4.3 Zhou-Gollmann协议的分析
6.5 两种形式化分析方法的比较
6.6 总结
习题
第7章 其他类型的安全协议
7.1 零知识证明技术与零知识协议
7.1.1 基本概念
7.1.2 Quisquater-Guillon零知识协议
7.1.3 Hamilton回路零知识协议
7.2 Feige-Fiat-Shamir身份识别协议
7.3 其他识别协议
7.3.1 Schnorr识别协议
7.3.2 Okamoto识别协议
7.4 智力扑克协议
7.4.1 基本概念
7.4.2 Shamir-Rivest-Adleman智力扑克协议
7.4.3 Shamir-Rivest-Adleman智力扑克协议的安全性分析
7.5 健忘传送协议
7.5.1 基本概念
7.5.2 Blum健忘传送协议
7.5.3 Blum健忘传送协议的安全性分析
7.5.4 公正掷币协议
7.6 密钥管理协议
7.6.1 Shamir门限方案
7.6.2 Asmuth-Bloom门限方案
7.6.3 Diffie-Hellman密钥交换协议
7.6.4 Matsumoto-Takashima-Imai密钥协商协议
7.7 总结
习题
第8章 Rubin逻辑
8.1 Rubin逻辑简介
8.2 应用Rubin逻辑规范协议
8.2.1 全局集合
8.2.2 局部集合
8.2.3 信任矩阵
8.2.4 关于临时值的注记
8.2.5 动作
8.2.6 Update函数
8.2.7 推理规则
8.3 应用Rubin逻辑分析协议
8.4 适用于非对称加密体制的Rubin逻辑
8.4.1 非对称加密体制的特点
8.4.2 密钥绑定
8.4.3 动作
8.4.4 Update函数
8.4.5 推理规则
8.5 总结
习题
第9章 典型的实用协议——SSL协议
9.1 SSL协议简介
9.1.1 SSL协议的发展过程
9.1.2 SSL协议的分层结构
9.1.3 SSL协议支持的密码算法
9.1.4 SSL协议的通信主体
9.2 SSL协议中的状态
9.2.1 会话状态和连接状态
9.2.2 预备状态和当前操作状态
9.3 记录协议层
9.3.1 工作流程
9.3.2 MAC的生成方法
9.4 change cipher spec协议
9.5 Alert协议
9.5.1 Close_notify消息
9.5.2 Error alerts消息
9.6 握手协议层
9.6.1 握手过程
9.6.2 握手消息
9.7 应用数据协议
9.8 密钥生成
9.8.1 通过pre_master_secret生成master_secret
9.8.2 通过master_secret生成MAC秘密、密钥和IVs
9.9 关于验证
9.10 总结
习题
第10章 SSL协议的安全性分析
10.1 针对SSL协议的攻击
10.1.1 穷尽搜索40位RC4密钥的攻击
10.1.2 利用RSA PKCS#1编码方法的脆弱性获得pre-master secret的攻击
10.2 从技术实现的角度分析SSL协议的安全性
10.2.1 握手协议层的安全性
10.2.2 记录协议层的安全性
10.3 SSL协议的形式化分析
10.3.1 形式化分析工具的选择
10.3.2 Rubin逻辑的简要回顾
10.3.3 应用Rubin逻辑规范SSL协议
10.3.4 应用Rubin逻辑分析SSL协议的模式1
10.4 总结
习题
第11章 串空间模型
11.1 简介
11.2 串空间模型基础
11.2.1 串空间模型的基本概念
11.2.2 丛和结点间的因果依赖关系
11.2.3 项与加密
11.2.4 自由假设
11.3 串空间模型中的攻击者
11.3.1 攻击者串
11.3.2 攻击者的一个界
11.4 正确性的概念
11.5 串空间模型分析方法举例
11.5.1 NSL串空间
11.5.2 一致性:响应者的保证
11.5.3 NSPK协议
11.5.4 机密性:响应者的临时值
11.5.5 机密性与一致性:发起者的保证
11.6 理想与诚实
11.6.1 理想
11.6.2 入口点与诚实
11.6.3 对攻击者的更多的界限
11.7 Otway-Rees协议
11.7.1 Otway-Rees协议的串空间模型
11.7.2 Otway-Rees协议的“机密性”
11.7.3 Otway-Rees协议的“认证性”
11.8 总结
习题
第12章 安全协议的新进展
12.1 CSP模型与分析方法
12.1.1 进程
12.1.2 CSP模型中的操作符
12.1.3 CSP方法中的迹模型
12.1.4 CSP模型分析梗概
12.1.5 CSP模型分析举例
12.2 串空间理论的进一步发展
12.2.1 认证测试方法
12.2.2 应用串空间模型方法进行分析
12.2.3 两种分析方法的比较
12.3 串空间模型与BAN类逻辑
12.4 其他安全协议分析方法
12.4.1 推理证明方法
12.4.2 证明构造方法
12.4.3 基于协议迹的分析方法
12.5 安全协议的设计
12.5.1 安全协议的设计原则
12.5.2 应用形式化方法指导安全协议设计
12.6 安全协议的发展与展望
12.6.1 形式化模型的粒度与应用范围
12.6.2 安全协议的其他重要问题
12.6.3 安全协议研究的公开问题与发展趋势
12.7 总结
习题
参考文献