安全协议理论与方法PDF电子书下载

第1章 引论 1

1.1 密码体制 1

1.1.1 基本原理 1

1.1.2 对称密钥密码体制 1

1.1.3 公钥密码体制 1

1.2 数字签名 2

1.2.1 数字签名(Digital Signature)技术 2

1.2.2 数字签名技术与加密技术的结合 3

1.2.3 几种新型的数字签名方案 3

1.3 Hash函数 5

1.4 密钥管理与分配 6

1.4.1 密钥的管理 6

1.4.2 密钥的分配 7

1.4.3 公钥证明书 8

1.5 PKI公钥基础设施 9

第2章 安全协议 13

2.1 安全协议概述 13

2.1.1 安全协议的概念 13

2.1.2 安全协议系统模型 14

2.1.3 安全协议的安全性质及实现 16

2.2 安全协议的缺陷 17

2.2.1 协议设计准则 18

2.2.2 安全协议缺陷分类 19

2.2.3 消息重放攻击及对策 21

2.3 安全协议及其受到的攻击实例 24

2.3.1 无可信第三方参与的对称密钥协议 24

2.3.2 有可信第三方参与的对称密钥协议 26

2.3.3 无可信第三方参与的公钥协议 35

2.3.4 有可信第三方参与的公钥协议 36

2.3.5 其他相关协议 39

2.4 安全协议的形式化分析 41

2.4.1 安全协议形式化分析概述 41

2.4.2 安全协议形式化分析的历史与现状 41

2.4.3 有关问题 43

小结 46

第3章 基于推理结构性方法 47

3.1 BAN逻辑 47

3.1.1 BAN逻辑的基本框架 48

3.1.2 应用实例 51

3.1.3 BAN逻辑的缺陷 54

3.1.4 BAN逻辑的设计准则 57

3.2 GNY逻辑 58

3.2.1 GNY逻辑的简单计算模型 58

3.2.2 GNY逻辑的语法和语义 59

3.2.3 GNY逻辑的推理规则 59

3.2.4 GNY逻辑对协议的分析 62

3.3 AT逻辑 63

3.3.1 AT逻辑的基本符号 64

3.3.2 AT逻辑的推理规则和公理 64

3.3.3 AT逻辑的计算模型 66

3.3.4 AT逻辑的语义 67

3.4 SVO逻辑 68

3.4.1 SVO逻辑的基本结构 69

3.4.2 SVO逻辑的推理规则及公理 69

3.4.3 SVO逻辑语义 71

3.4.4 SVO逻辑的应用实例 73

3.5 Kailar逻辑 79

3.5.1 Kailar逻辑的基本架构 79

3.5.2 Kailar逻辑的应用实例 82

3.5.3 Kailar逻辑的缺陷 85

3.6 CS逻辑 86

3.6.1 逻辑框架 87

3.6.2 CS逻辑的扩展 88

3.6.3 实例分析 91

3.7 KG逻辑 95

3.7.1 基本标记与假设 95

3.7.2 推理规则 96

3.7.3 实例分析 98

3.8 Nonmonotomic逻辑 100

3.8.1 基本符号和逻辑框架 100

3.8.2 推理规则 105

3.8.3 协议分析流程 105

小结 107

第4章 基于攻击结构性方法 108

4.1 一般目的的验证语言 108

4.1.1 一阶谓词逻辑扩展 108

4.1.2 Murφ验证系统 111

4.1.3 CSP与安全性质 113

4.1.4 Model Checking 123

4.2 单一代数理论模型 138

4.2.1 Dolev-Yao模型 139

4.2.2 Merritt模型 140

4.2.3 Meadows模型 140

4.2.4 Woo-Lam模型 144

4.3 特别目的的专家系统 146

4.3.1 Interrogator 146

4.3.2 NRL协议分析器 147

4.3.3 基于规则系统 151

小结 152

第5章 基于证明结构性方法 153

5.1 human-readable证明法 153

5.1.1 主体知识及操作 153

5.1.2 协议形式化分析实例 156

5.1.3 并行多重会话 160

5.2 Paulson归纳法 161

5.2.1 归纳法概述 162

5.2.2 归纳法的自动化理论 167

5.2.3 归纳法对一个递归协议的分析 171

5.3 Schneider秩函数 175

5.3.1 秩函数的定义 175

5.3.2 主要定理 176

5.3.3 实例分析 177

5.3.4 新版秩函数 182

5.4 strand space 183

5.4.1 理论框架 184

5.4.2 攻击者 188

5.4.3 协议的正确性 190

5.4.4 NSL协议分析 191

5.4.5 ideal 195

5.4.6 对Otway-Rees协议的分析 196

5.5 Attacks限定法 200

5.5.1 认证协议模型 200

5.5.2 限定 205

5.5.3 约简定理 207

5.6 Rewriting逼近法 208

5.6.1 预备知识 208

5.6.2 逼近技术 209

5.6.3 对NS公钥协议和攻击者的编码 211

5.6.4 逼近和验证 214

5.7 Maude分析法 216

5.7.1 Maude的面向对象的说明 217

5.7.2 NS公钥协议的说明与执行 217

5.7.3 攻击者和一个攻击 220

5.7.4 宽度优先搜索策略 221

5.8 invariant技术 222

5.8.1 基本概念 223

5.8.2 描述攻击者不可知术语集合属性的不变式 224

5.8.3 描述攻击者可知消息集合属性的不变式 226

小结 227

第6章 安全协议分析的形式化语言 229

6.1 安全协议分析语言：CPAL 229

6.1.1 CPAL行为的含义 230

6.1.2 CPAL的语法 231

6.1.3 CPAL的形式化语义 232

6.1.4 CPAL协议评估系统 236

6.1.5 使用CPAL评估系统对协议进行验证 238

6.2 安全协议简单接口说明语言——ISL ＆ AAPA 242

6.2.1 ISL定义 243

6.2.2 AAPA的输出 248

6.2.3 与基于攻击结构性工具的比较 250

6.3 安全协议通用说明语言——CAPSL 251

6.3.1 CAPSL集成环境 252

6.3.2 CAPSL 252

6.3.3 分析工具接口格式 258

6.3.4 翻译器算法 262

6.3.5 安全协议的分析 263

6.4 安全协议分析编译器Casper 267

6.4.1 Casper的语法 267

6.4.2 Casper的实施 272

6.4.3 实例分析：大嘴青蛙(WMF)协议 276

6.4.4 与CAPSL的比较 280

6.5 安全协议的积分——spi积分 281

6.5.1 使用限制性信道的协议 281

6.5.2 使用密码体制的协议 285

6.5.3 spi积分的形式化语义 290

小结 292

第7章 安全协议设计的形式化方法 293

7.1 Heintze ＆ Tygar：模型及其构成 293

7.1.1 模型和安全性 294

7.1.2 协议和非记时模型 296

7.1.3 协议的组合 299

7.2 Gong ＆ Synersion：fail-stop协议 300

7.2.1 fail-stop协议及其分析 301

7.2.2 方法的应用 304

7.2.3 fail-safe协议 306

7.2.4 使用因果一致性概念的形式化 308

7.3 Buttyan ＆ Staaman简单逻辑 308

7.3.1 模型 308

7.3.2 简单逻辑 310

7.3.3 分析和修正Woo ＆ Lam认证协议 314

7.4 Rudolph抽象模型 317

7.4.1 原理 317

7.4.2 抽象协议的APA模型 319

7.4.3 协议级联 322

小结 324

第8章 Kerberos 325

8.1 Kerberos协议概况 325

8.1.1 cross-realm操作 327

8.1.2 通信主体的选择 328

8.1.3 授权 328

8.1.4 环境假设 328

8.1.5 术语 329

8.2 票据标志使用与请求 329

8.3 消息交换 331

8.3.1 认证服务交换 331

8.3.2 客户/服务器认证交换 333

8.3.3 TGS交换 334

8.3.4 KRB_SAFE交换 335

8.4 ULTRIX操作系统上Kerberos的实现 336

第9章 IPSec协议 340

9.1 IPSec体系结构 340

9.2 安全联盟 341

9.3 IPSec的安全协议 342

9.3.1 IPSec的模式 343

9.3.2 封装安全载荷(ESP) 343

9.3.3 认证头(AH) 346

9.4 IPSec的应用 348

第10章 SSL V3.0 350

10.1 SSL V3.0概况 350

10.1.1 SSL V3.0的特点 350

10.1.2 SSL V3.0的结构 351

10.1.3 SSL V3.0的加密属性 352

10.1.4 SSL V3.0的通信主体 352

10.2 SSL V3.0中的状态 352

10.2.1 会话状态和连接状态 352

10.2.2 预备状态和当前操作状态 353

10.3 记录层协议 354

10.4 Change Cipher Spec协议 356

10.5 Alert协议 356

10.5.1 clase_notify消息 356

10.5.2 error alerts消息 356

10.6 握手协议层 356

第11章 X.509 360

11.1 X.509 v3证书概述 360

11.1.1 证书路径和信任 361

11.1.2 撤消 361

11.1.3 操作协议/管理协议 362

11.2 证书及其扩展 363

11.2.1 基本证书域 363

11.2.2 标准证书扩展 366

11.3 CRL及其扩展 373

11.3.1 CRL域 373

11.3.2 CRL扩展 374

11.3.3 CRL输入项扩展 376

11.4 证明路径的检验 377

11.4.1 基本路径检验 377

11.4.2 扩展路径检验 379

11.5 算法支持 379

11.5.1 单向Hash函数 379

11.5.2 签名算法 380

11.5.3 公钥加密算法 381

第12章 SET协议 384

12.1 背景及商业要求 385

12.2 系统设计 387

12.2.1 SET系统结构 389

12.2.2 安全服务及证书 391

12.2.3 技术要求 392

12.3 证书管理结构 395

12.4 证书请求协议 396

12.4.1 主协议 396

12.4.2 持卡人证书发起请求/响应处理 397

12.4.3 持卡人注册表单请求/响应处理 398

12.4.4 商家/支付网关证书发起处理 400

12.4.5 证书请求和生成处理 402

12.4.6 证书质询及状态处理 406

12.5 证书撤消 407

12.5.1 持卡人证书的撤消 407

12.5.2 商家证书撤消 407

12.5.3 支付网关证书撤消 408

12.5.4 CA崩溃恢复 408

12.6 SET私有扩展 409

12.6.1 HashedRootKey私有扩展 409

12.6.2 CertificateType私有扩展 409

12.6.3 VIerchantData私有扩展 410

12.6.4 CardCertRequired私有扩展 411

12.6.5 Tunneling私有扩展 411

12.6.6 SETExtensions私有扩展 411

参考文献 412