为了保障电子商务活动中各方的利益不被侵害,需要利用基于密码技术的电子商务协议来保证商务活动的安全性,因此对电子商务协议的安全性的形式化分析是一个至关重要的有难度的问题。针对电子商务协议安全性的形式化分析方法的研究晚于对传统的密码协议的形式化分析方法的研究,目前主要的分析方法有：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协议的分析中发现非诚实的投票人能够篡改投票结果并能够控制协议是否终止本文最后研究了公平交换协议的一种基础签名算法——并发签名,提出并定义了并发签名的可追踪性以保证签名方与签署消息之间的唯一绑定关系,防止签名被滥用。基于学者王贵林提出的一个完美并发签名方案,本文设计了一个满足可追踪性的并发签名方案,并基于此方案设计了一个无需第三方的公平交换协议。