【作者】 李云峰；

【导师】 何大可；

【作者基本信息】 西南交通大学 ， 交通信息工程与控制， 2009， 博士

【摘要】 为了保障电子商务活动中各方的利益不被侵害,需要利用基于密码技术的电子商务协议来保证商务活动的安全性,因此对电子商务协议的安全性的形式化分析是一个至关重要的有难度的问题。针对电子商务协议安全性的形式化分析方法的研究晚于对传统的密码协议的形式化分析方法的研究,目前主要的分析方法有：Kailar逻辑,SVO逻辑,基于SMV的模型检测,基于ATL／ATS博弈逻辑系统的分析方法,以及卿斯汉等学者提出的对两方或者多方电子商务协议和公平交换协议进行分析、证明的方法。这些方法分别从协议的消息语义、协议结构角度对协议进行建模与分析。综合考虑协议的消息和结构两个因素的形式化分析方法较少。当前,对电子商务协议的形式化分析方法的研究依然是一个热点领域。本文首先对主要的博弈逻辑：ATL逻辑、ATEL逻辑、ATL-A／ATEL-A逻辑、多代理逻辑等,进行了研究,发现他们对博弈主体的状态转移的建模方式采用固定的步骤。本文提出了一个智能代理博弈主体模型(IA),在IA中,一个博弈主体的状态由博弈主体根据其接收的消息按照逻辑推理规则进行状态的更新,在每一个状态下,根据推理规则推演出当前可发送消息集合。多个IA构成了一个基于消息的并发博弈系统(MCGS),这个系统中每一步的迁移是通过两个动作完成,分别是：各个IA的收发消息,以及各IA根据自己接收的消息按逻辑推理规则更新自身状态。整个系统的策略使用基于ATL扩展的ATL-B逻辑进行表达。IA,MCGS,ATL-B共同构成了一个对系统进行建模的工具,称为MIAG(多智能体博弈)系统,这个系统的特点是各博弈主体之间只通过消息交互,每个主体有自己的认知推理逻辑规则用以更新状态,与其他博弈逻辑相比,博弈主体具有动态的状态迁移特性。基于MIAG模型,本文构建了一个电子商务协议分析的新模型,其主要特点是在博弈主体中引入了针对电子商务协议的逻辑推理规则用于更新博弈主体的认知状态；使用ATL-B策略公式表达不同的安全目标,使其能够适应对不同目的的电子商务协议的建模要求。在新模型中,将协议主体分成诚实主体与非诚实主体两个集合,分析过程依次针对诚实主体的各个协议运行迹分析非诚实方是否存在攻击策略。本文总结了四种典型的非诚实方攻击策略,使得本文的分析模型能够比之前的模型更切合实际的形式化非诚实主体的能力。应用电子商务协议分析的新模型,本文对一个公平交换协议Nenadi04和一个无需中央机构的电子投票协议Su-Vote协议进行了分析,发现了协议中存在的漏洞,说明了新模型的有效性。在对Nenadi04协议的分析中,利用新模型发现了发方不可否认证据不满足可追究性的要求,也发现了协议中发起方可以利用并发多个协议实例来混淆应答方对恢复子协议接收消息的识别,从而破坏协议的公平性。这个协议实例说明了新模型能够同时处理对消息和协议结构的分析。对Su-Vote协议的分析中发现非诚实的投票人能够篡改投票结果并能够控制协议是否终止本文最后研究了公平交换协议的一种基础签名算法——并发签名,提出并定义了并发签名的可追踪性以保证签名方与签署消息之间的唯一绑定关系,防止签名被滥用。基于学者王贵林提出的一个完美并发签名方案,本文设计了一个满足可追踪性的并发签名方案,并基于此方案设计了一个无需第三方的公平交换协议。更多还原

【Abstract】 E-commerce protocol is designed to fulfill business flow and prtotect the attender’s profit using cryptography technical. So, it is a common sense that the formal analysis of the security of E-commerce protocols is an important and difficult problem.The study of formal analysis methods for E-commerce protocol security is later than that for traditional cryptographic protocol. There are many active formal analysis methods for E-commerce protocol, such as:Kailar logic, SVO logic, model checking using SMV, game analysis based on ATL/ATS system and methods proposed by Prof. Si-Han Qing, which could be used to analyze or prove the security of two party or multiple party fair exchange protocols. Some of these methods focus on the analysis of the message or focus on the structure of the protocol. Few formal analysis method could consider the message and the structure of a protocol at the same time. At present, formal analysis methods of E-commerce protocol is still a hot research area.The first part of this paper researchs the major game logic systems, for example:ATL, ATEL, ATL-A/ATEL-A, MMAL, and found that these game logic system model the status of game agent with fixed state machine. Based on this finding, IA(Intelligent Agent) model is proposed, in which the agent update its status based on message he received and the logical inference rules. And in every status, the agent reason about what could he send using the inference rules. Multiple IAs constitute one MCGS(Message based Concurrent Game System). ATL-B, which includes epistemic logic propositions, extended from ATL, is used to model the system strategies. IA, MCGS, ATL-B together constitute a tool of modeling the system, known as the MIAG (Multiple Intelligent Agent Game) system which is characterized by that the game agent interact through message only and each agent has its own logical inference rules for the renewal of its state.In the second part, Using MIAG, this paper built a new E-commerce protocol analysis model, in which the game agent update its epistemic state using the logical inference rules; ATL-B strategy formula could express different security goals, for different E-commerce protocol. In the new model, participates are divided into honest agent set and dishonest agent set. Then, given every trace of the honest agent in the target protocol, the strategy of dishonest agent are analyzed to check weather it has strategy to get more benefit then the honest agent. In this paper, four typical attack strategies are identified which is more reality then those defined in the other formal analysis methods proposed before.In third part, one fair exchange protocol, Nenadi04, and one non-central E-voting protocol, Su-Vot are analysised using the new model. Flaws are found in these protocols, which confirmed the validity of the new model. When analyzing Nenadi04, we found that the non-repudiation evidence dose not satisfy accountability and also, the initiator of Nenadi04 could launch a number of recovery sub-protocols to confuse the responder with messages for different instance, thereby break the fairness of Nenadi04. The analysis of Nenadi04 exemplified that the new model could analyze fair exchange protocols from both the message and structure point of view at the same time. The dishonest voter in Su-Vote protocol could modify the voting result and have strategy to control weather the protocol could finish in time.In the last part of this paper, we propose and define the traceability of concurrent signature to bind the signer and message together to prevent the abuseness. Based on improved Perfect Concurrent Signature proposed by Guilin Wang, this paper designed one concurrent signature scheme, which satisfy the traceability, based on which one fair exchange protocol without trusted third party is proposed.更多还原