电子商务协议形式化分析工具的研究

摘要

随着电子商务在全球的迅猛发展，电子商务的安全问题日益受到人们的关注。安全的电子商务协议是确保电子商务活动可靠开展的基础，而安全协议的形式化分析逻辑则是检验协议是否安全的有力工具。　　本文首先介绍了电子商务协议的多层安全需求模型，以及安全电子商务协议中涉及的关键基础技术。在此基础之上，本文以最典型的BAN逻辑和Kailar逻辑为例，对已有的形式化逻辑工具进行了深入的分析，以具体的协议分析实例说明了它们存在的不足和缺陷，并针对这些不足和缺陷提出了一种新的形式化逻辑工具。新工具通过对分析步骤的规范和改进，在一定程度上避免了由于不恰当的假设、不合理的理想化等原因导致的错误分析；通过引入了“协议的本次执行”这一概念，能够有效地分析出BAN逻辑所无能为力的重放攻击；通过对“可追究法则”的改进和扩充，克服了Kailar逻辑无法分析签名密文的缺陷；通过增加“密钥判断法则”，能够形式化地证明密钥的性能，有效地弥补了BAN逻辑在这方面的缺陷。新的逻辑工具可以分析协议主体间的信任关系和可追究关系，可用于分析电子商务协议、认证协议以及密钥分配协议等。本文最后通过一系列具体的安全协议分析实例，验证了新工具的性能。

目录

文摘

英文文摘

南京邮电学院学位论文独创性声明及南京邮电学院学位论文使用授权声明

前言

第一章电子商务协议及形式化分析技术

1.1电子商务及其协议

1.1.1电子商务

1.1.2电子商务协议

1.1.3电子商务协议的分类

1.1.4电子商务协议的安全需求模型

1.2安全协议的形式化分析技术

第二章安全电子商务协议的技术理论基础

2.1密码技术

2.1.1密码系统概述

2.1.2对称密码体制

2.1.3非对称密码体制

2.1.4数字信封技术

2.2 PKI相关技术

2.2.1消息摘要

2.2.2数字签名

2.2.3公钥证书

2.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.2.3对Kailar逻辑的讨论

3.3其它电子商务形式协议化分析逻辑

第四章一种新的形式化分析逻辑

4.1新逻辑的形式化分析体系结构

4.1.1新逻辑的基本构造

4.1.2新逻辑的推理规则

4.1.3新逻辑的推理步骤

4.2新逻辑的形式化分析实例

4.2.1分析Otway-Rees协议

4.2.2分析Nessett协议

4.2.3分析CMP1、CMP1(b)协议

4.2.4分析Zhou-Gollman协议

总结与展望

致谢

参考文献

本人已录用的论文