电子商务网络协议的形式化分析理论与应用PDF电子书下载

第1章 概论 1

1.1 信息安全的基本定义 1

1.2 网络的安全问题 1

1.3 网络安全体系结构 3

第2章 电子商务协议的形式化分析理论基础 7

2.1 电子商务的定义 7

2.2 电子商务协议的安全性 7

2.2.1 电子商务协议的安全性 7

2.2.2 电子商务协议的设计原则 9

2.2.3 电子商务协议的安全分析 11

2.2.4 电子商务协议形式化分析方法分类 11

第3章 电子商务协议的形式化逻辑分析方法 15

3.1 BAN逻辑 15

3.1.1 BAN逻辑公式 15

3.1.2 BAN逻辑的推理规则 16

3.1.3 BAN逻辑的评价 16

3.2 Kailar逻辑 17

3.2.1 Kailar逻辑公式 17

3.2.2 Kailar逻辑的推理规则 18

3.3 NDL逻辑 19

3.3.1 NDL逻辑的语法 19

3.3.2 NDL逻辑的推理规则 20

3.4 卿周逻辑 21

3.4.1 卿周逻辑的语法 21

3.4.2 卿周逻辑的推理规则 22

第4章 电子商务协议的通用形式化Petri网模型分析方法 24

4.1 Petri网概述 24

4.2 Petri网的定义 24

4.3 Petri网的应用实例 25

4.4 Petri网的特性 26

4.4.1 保守网 26

4.4.2 有界网 27

4.4.3 活动性 29

4.4.4 并发与冲突 29

4.5 Petri网的扩充 29

4.5.1 输入函数和输出函数的扩充 29

4.5.2 触发条件的扩充 30

4.5.3 旗标和库所的扩充（着色Petri网） 30

4.6 Petri网的替换与合成 30

4.7 常用的Petri网模型 31

4.7.1 库所／变迁网（P/T网）的形式化定义 31

4.7.2 有色网的形式化定义 32

4.7.3 常量弧有色网的形式化定义 32

4.8 Petri网的分析 33

4.8.1 常量弧网 33

4.8.2 库所／变迁网（P/T网） 37

4.8.3 有色网 39

第5章 电子商务协议的形式化有穷自动机模型检测分析方法 42

5.1 有穷自动机的定义 42

5.2 传输通道类别 43

5.3 通道DFA 44

5.4 协议实体DFA 46

5.5 DFA的简化 47

5.6 DFA的合成 48

第6章 基于电子商务安全认证和交易的基本协议 52

6.1 安全认证的基本协议 52

6.1.1 Needham-Schroeder认证协议 52

6.1.2 Kerberos认证协议 53

6.1.3 Otwag-Rees认证协议 55

6.2 电子交易的基本协议 56

6.2.1 网上交易协议遵循的原则 56

6.2.2 IBS支付协议 57

6.2.3 CMP1及CMP2非否认协议 58

6.2.4 Zhou-Gollman非否认协议 58

6.2.5 ISO非否认协议M2 59

6.2.6 卿斯汉非否认协议 59

6.2.7 ISI支付协议 60

6.2.8 SSL（安全套接层协议） 61

6.2.9 SET协议 62

6.2.10 PGP（Pretty Good Privacy）协议 63

第7章 基于公钥基础设施PKI的安全认证协议 64

7.1 PKI安全体系结构 64

7.2 安全认证体系结构标准X.509 65

7.2.1 X.509的简单认证程序 66

7.2.2 X.509的强认证程序 67

7.2.3 X.509的证书内容 67

7.3 安全认证的目录存取协议LDAP 69

第8章 基于工商管理的安全认证协议 71

8.1 认证协议的用户需求 71

8.2 安全认证协议的功能和机制 72

8.3 安全认证协议的协议元素 74

8.4 认证协议的形式化规定 76

8.5 单向认证协议 76

8.6 双向认证协议 77

第9章 安全认证协议的Petri网模型 79

9.1 单向认证协议的Petri网模型 79

9.1.1 构建A主体Petri网模型A 79

9.1.2 构建S主体Petri网模型S 80

9.1.3 构建B主体Petri网模型B 81

9.1.4 A、B、S Petri网模型的合并 81

9.2 双向认证协议的Petri网模型 82

9.3 安全认证协议模型的仿真分析 86

9.3.1 认证协议的要素 86

9.3.2 安全认证协议的描述语言 88

9.3.3 单向安全认证协议的具体仿真及实现 93

9.3.4 双向认证协议的具体仿真及实现 98

第10章 支付协议的有穷自动机模型 102

10.1 支付协议 102

10.2 工商支付协议的形式化描述 102

10.3 支付协议的有穷自动机模型 103

10.4 支付协议满足不可否认性的仿真分析 105

10.5 支付协议满足公平性的仿真分析 107

第11章 协议的有色Petri网模型及分析 112

11.1 CP_Net简介 112

11.2 CPN Tools简介 112

11.2.1 CPN Tools安装 113

11.2.2 CPN Tools界面 113

11.2.3 CPN Tools文件格式 113

11.2.4 CPN网络的载入、创建与保存 114

11.3 CPN ML语言 114

11.3.1 标识符 114

11.3.2 颜色集 115

11.3.3 变量 118

11.3.4 函数 119

11.3.5 常量 120

11.4 CPN网的有关操作 121

11.4.1 网络编辑 121

11.4.2 添加／编辑声明 121

11.4.3 添加／编辑标注 122

11.4.4 文本编辑 123

11.4.5 布局编辑 123

11.4.6 有色Petri网的分析 123

11.5 协议的Petri网模型 127

11.5.1 Needham-Schroedor公钥认证协议 127

11.5.2 Needham-Schroedor公钥认证协议的Petri网模型 128

11.6 基于Petri网模型的安全协议分析方法 130

11.6.1 基于Petri网的安全协议分析方法和步骤 130

11.6.2 NS协议的分析 132

11.7 用CPN tools工具来分析协议 137

11.7.1 用CPN tools工具分析协议的方法和步骤 138

11.7.2 用CPN tools工具来分析Needham-Schroedor公钥认证协议 138

参考文献 145