电子商务协议安全性形式化分析方法的研究

《电子商务协议安全性形式化分析方法的研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、西南交通大学博士学位论文电子商务协议安全性的形式化分析方法研究姓名：李云峰申请学位级别：博士专业：交通信息工程与控制指导教师：何大可20090501西南交通大学博士学位论文第1页摘要为了保障电子商务活动中各方的利益不被侵害，需要利用基于密码技术的电子商务协议来保证商务活动的安全性，因此对电子商务协议的安全性的形式化分析是一个至关重要的有难度的问题。针对电子商务协议安全性的形式化分析方法的研究晚于对传统的密码协议的形式化分析方法的研究，目前主要的分析方法有：Kailar逻辑，SV0逻辑，基于SMV的模型检测，基于ATL／ATS博弈逻辑系统的分析方法，以及卿斯

2、汉等学者提出的对两方或者多方电子商务协议和公平交换协议进行分析、证明的方法。这些方法分别从协议的消息语义、协议结构角度对协议进行建模与分析。综合考虑协议的消息和结构两个因素的形式化分析方法较少。当前，对电子商务协议的形式化分析方法的研究依然是一个热点领域。本文首先对主要的博弈逻辑：ATL逻辑、ATEL逻辑、ATL．A／ATEL-A逻辑、多代理逻辑等，进行了研究，发现他们对博弈主体的状态转移的建模方式采用固定的步骤。本文提出了一个智能代理博弈主体模型(认)，在认中，一个博弈主体的状态由博弈主体根据其接收的消息按照逻辑推理规则进行状态的更新，在每一个状态下，根

3、据推理规则推演出当前可发送消息集合。多个队构成了一个基于消息的并发博弈系统(MCGS)，这个系统中每一步的迁移是通过两个动作完成，分别是：各个队的收发消息，以及各认根据自己接收的消息按逻辑推理规则更新自身状态。整个系统的策略使用基于ATL扩展的ATL．B逻辑进行表达。n，MCGS，ATL．B共同构成了一个对系统进行建模的工具，称为MLAG(多智能体博弈)系统，这个系统的特点是各博弈主体之间只通过消息交互，每个主体有自己的认知推理逻辑规则用以更新状态，与其他博弈逻辑相比，博弈主体具有动态的状态迁移特性。基于MIAG模型，本文构建了一个电子商务协议分析的新模型

4、，其主要特点是在博弈主体中引入了针对电子商务协议的逻辑推理规则用于更新博弈主体的认知状态；使用ATLoB策略公式表达不同的安全目标，使其能够适应对不同目的的电子商务协议的建模要求。在新模型中，将协议主体分成诚实主体与非诚实主体两个集合，分析过程依次针对诚实主体的各个协议运行迹分析非诚实方是否存在攻击策略。本文总结了四种典型的非诚实方攻击策略，使得本文的分析模型能够比之前的模型更切合实际的形式化非诚实主体的能力。应用电子商务协议分析的新模型，本文对一个公平交换协议Nenadi04和第1I页西南交通大学博士学位论文一个无需中央机构的电子投票协议Su．Vote协

5、议进行了分析，发现了协议中存在的漏洞，说明了新模型的有效性。在对Nenadi04协议的分析中，利用新模型发现了发方不可否认证据不满足可追究性的要求，也发现了协议中发起方可以利用并发多个协议实例来混淆应答方对恢复子协议接收消息的识别，从而破坏协议的公平性。这个协议实例说明了新模型能够同时处理对消息和协议结构的分析。对Su．Vote协议的分析中发现非诚实的投票人能够篡改投票结果并能够控制协议是否终止。本文最后研究了公平交换协议的一种基础签名算法一并发签名，提出并定义了并发签名的可追踪性以保证签名方与签署消息之间的唯一绑定关系，防止签名被滥用。基于学者王贵林提出

6、的一个完美并发签名方案，本文设计了一个满足可追踪性的并发签名方案，并基于此方案设计了一个无需第三方的公平交换协议。关键词电子商务协议，博弈逻辑，形式化方法，并发签名，公平性，可追究性，电子投票，公平交换西南交通大学博士学位论文第1II页AbstractE—commerceprotocolisdesignedtofulfillbusinessflowandprtotecttheattender’Sprofitusingcryptographytechnical．So，itisacommonsensethattheformalanalysisofthesecu

7、rityofE—commerceprotocolsisanimportantanddifficultproblem．ThestudyofformalanalysismethodsforE—commerceprotocolsecurityislaterthanthatfortraditionalcryptographicprotoc01．TherearemanyactiveformalanalysismethodsforE—commerceprotocol，suchas：Kailarlogic，SVOlogic，modelcheckingusingSMV，g

8、ameanalysisbasedonATL／ATSsysteman