信息技术改变着人们的生活和工作方式，社会的信息化程度大大提高，信息产业成为世界第一大产业。信息的获取、处理和安全保障能力成为一个国家综合国力的重要组成部分。

该书针对目前电子商务协议研究中重视加密技术而忽视协议逻辑设计的问题，采用形式化的分析工具来精确描述和仿真协议的行为，验证协议能否达到预期的目标，从而确保电子商务协议设计的正确性。

该书的主要内容包括：电子商务协议的形式化逻辑分析方法、通用形式化Petri网模型分析方法、有穷自动机模型检测分析方法、安全认证和交易的基本协议，以及协议的有色Petri网模型及分析的软件工具CPN T001s等。同时，该书应用这些分析方法和工具，对相关的认证和支付协议进行了具体分析。

本书叙述了与信息安全有密切联系的基于网络电子商务协议的形式化分析理论方法与实际应用。具体内容包括：电子商务协议的形式化逻辑分析方法、通用形式化Petri网模型分析方法、有穷自动机模型检测分析方法、安全认证和交易的基本协议，以及协议的有色Petri网模型及分析的软件工具CPN Tools等。同时，本书应用这些分析方法和工具具体分析了相关的认证和支付等协议。

本书适合于高等院校计算机专业、电子商务专业高年级本科生和研究生阅读，也可供科研人员参考。

序

前言

第1章 概论

 1.1 信息安全的基本定义

 1.2 网络的安全问题

 1.3 网络安全体系结构

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

 2.1 电子商务的定义

 2.2 电子商务协议的安全性

2.2.1 电子商务协议的安全性

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

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

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

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

 3.1 BAN逻辑

3.1.1 BAN逻辑公式

3.1.2 BAN逻辑的推理规则

3.1.3 BAN逻辑的评价

 3.2 Kailar逻辑

3.2.1 Kailar逻辑公式

3.2.2 Kailar逻辑的推理规则

 3.3 NDL逻辑

3.3.1 NDL逻辑的语法

3.3.2 NDL逻辑的推理规则

 3.4 卿周逻辑

3.4.1 卿周逻辑的语法

3.4.2 卿周逻辑的推理规则

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

 4.1 Petri网概述

 4.2 Petri网的定义

 4.3 Petri网的应用实例

 4.4 Petri网的特性

4.4.1 保守网

4.4.2 有界网

4.4.3 活动性

4.4.4 并发与冲突

 4.5 Petri网的扩充

4.5.1 输人函数和输出函数的扩充

4.5.2 触发条件的扩充

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

 4.6 Petri网的替换与合成

 4.7 常用的Petri网模型

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

4.7.2 有色网的形式化定义

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

 4.8 Petri网的分析

4.8.1 常量弧网

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

4.8.3 有色网

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

 5.1 有穷自动机的定义

 5.2 传输通道类别

 5.3 通道DFA

 5.4 协议实体DFA

 5.5 DFA的简化

 5.6 DFA的合成

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

 6.1 安全认证的基本协议

6.1.1 Needham—Schroeder认证协议

6.1.2 Kerberos认证协议

6.1.3 Otwag—Rees认证协议

 6.2 电子交易的基本协议

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

6.2.2 IBS支付协议

6.2.3 CMP1及CMP2非否认协议

6．2．4 Zhou-Gollman非否认协议

6．2．5 IS0非否认协议M2 

6．2．6 卿斯汉非否认协议

6．2．7 ISL支付协议

6．2．8 SSL(安全套接层协议)

6．2．9 SKT协议

6．2．10 PGP(Pretty Good Privacy)协议

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

 7．1 PKI安全体系结构

 7．2 安全认证体系结构标准X．509

7．2．1 X.509的简单认证程序 

7．2．2 X.509的强认证程序

7．2．3 X.509的证书内容

 7．3安全认证的目录存取协议LDAP

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

 8．1 认证协议的用户需求

 8．2 安全认证协议的功能和机制

 8．3 安全认证协议的协议元素

 8．4 认证协议的形式化规定

 8．5 单向认证协议

 8．6 双向认证协议

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

 9．1 单向认证协议的Petri网模型

9．1．1 构建A主体Petri网模型A

9．1．2 构建s主体Petri网模型S

9．1．3 构建B主体Petii网模型B

9．1．4 A、B、s Petri网模型的合并

 9．2 双向认证协议的Petri网模型

 9．3 安全认证协议模型的仿真分析

9．3．1 认证协议的要素

9．3．2 安全认证协议的描述语言

9．3．3 单向安全认证协议的具体仿真及实现

9．3．4 双向认证协议的具体仿真及实现

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

 10．1 支付协议

 10．2 工商支付协议的形式化描述

 10．3 支付协议的有穷自动机模型

 10．4 支付协议满足不可否认性的仿真分析

 10．5 支付协议满足公平性的仿真分析

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

 11．1 CP－Net简介

 11．2 CPN Tools简介

11．2．1 CPN Tools安装

11．2．2 CPN Tools界面

11．2．3 CPN Tools文件格式

11．2．4 CPN网络的载人、创建与保存

 11．3 CPN ML语言

11．3．1 标识符

11．3．2 颜色集

11．3．3 变量

11．3．4 函数

11．3．5 常量

 11．4 CPN网的有关操作

11．4．1 网络编辑

11．4．2 添加／编辑声明 

11．4．3 添加／编辑标注 

11．4．4 文本编辑

11．4．5 布局编辑

11．4．6 有色Petri网的分析

 11．5 协议的Petri网模型

11．5．1 Needham-Schroedor公钥认证协议

11．5．2 Needham-Schroedor公钥认证协议的Petri网模型

 11．6 基于：Petri网模型的安全协议分析方法

11．6．1 基于Petri网的安全协议分析方法和步骤

11．6．2 NS协议的分析

 11．7 用CPN tools工具来分析协议

11．7．1 用CPN tools工具分析协议的方法和步骤

11．7．2 用cPN tools工具来分析：Needham-Schroedor公钥认证协议

参考文献