基于SPV逻辑的电子商务协议形式化分析与研究

摘要

随着计算机网络和电子商务的普及，网络安全问题越来越受到重视，而电子商务协议就是解决电子商务中网络安全问题的有效手段之一。虽然电子商务协议使用密码系统来确保其安全性，但是，它们中的漏洞很多时候是由于其设计中可能的逻辑错误所导致的，而不是由于其加密算法不可靠。所以使用逻辑推理的方法来分析电子商务协议变得十分重要，而且是研究的热点。 本文的理论基础来源于国家自然科学基金项目(认识逻辑及其在安全协议设计、验证中的应用，项目编号：60073056)所提出的SPV逻辑(Security Protocol Verifier Logic)。这是一种基于逻辑推理，而且高效的验证逻辑，并且有相应的自动验证工具SPV。 本文首先使用SPV逻辑分析了一类重要的电子商务协议——SET支付协议及其简化版本Lu-Smolka协议，指出了其存在漏洞的原因一是没有对订购信息OI和支付指令PI进行双重数字签名用以证明消息没有被篡改，二是没有对交易的各方进行通信主体的身份认证。然后在此结果上改进了Lu-Smolka协议，使用SPV逻辑分析后得出改进的协议比原协议满足更多的安全性质。 本文接着从另一个角度对电子商务协议的核心基础协议：公平非否认性协议展开研究。在验证和分析了已有的几个不同类型的公平非否认性协议之后，设计了一个新的基offline TTP的公平非否认性协议(Fair Non-Repudiation Protocols with Offiine Trusted Third Party)——FNR协议，然后对该协议使用SPV逻辑进行了手工和自动验证，证明该协议不仅很好满足的公平非否认性协议的设计目标，而且大大降低了由于第三方的不安全性带来的隐患，与目前已有的同类协议相比，FNR协议有更好的安全性质。此外，在研究公平非否认性协议的基础上，本文也第一次发现了SPV逻辑不完备性的实例，并提出了对其进行改进的建议。

目录

文摘

英文文摘

声明

第一章引言

1.1 安全协议的基本概念

1.2 安全协议形式化分析方法概述

1.3 电子商务协议及其研究现状

1.4 本文研究内容及结构

第二章SPV逻辑及其应用综述

2.1 概述

2.2 加密信息交换模型和实例化空间

2.3 基于局部会话的验证逻辑LLS

2.4 SPV逻辑的自动化验证工具——SPV简介

2.5 本章小结

第三章SET及其简化协议的验证与分析

3.1 SET协议及其简化协议简介

3.2 Lu-Smolka协议的形式化验证与分析

3.3 对Lu-Smolka协议的改进及形式化分析

3.4 本章小结

第四章公平非否认性协议的设计与研究

4.1 公平非否认性协议的进一步说明及其设计原则

4.2 经典公平非否认性协议及其形式化分析

4.3 一个新的公平非否认性协议——FNR协议的提出

4.4 FNR协议的形式化验证与分析

4.5 本章小结

第五章总结与展望

5.1 本文的工作与总结

5.2 进一步研究工作与展望

参考文献

致谢