电子商务协议形式化分析是电子商务研究的一个重要方面，电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础，其基本属性包括安全性、保密性、完整性、可认证性、非否认性及公平性等。进行电子商务协议的形式化分析研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术保障。 目前国内外对电子商务协议的分析验证手段主要有以下几种： (1)实际攻击验证方法； (2)从表面上进行直观检测； (3)形式化逻辑分析方法。 前两种方法存在较多缺点，如：属于事后检测，需在协议建立实施之后才能进行检测、检测手段不够严密等。而形式化逻辑分析方法可以在协议实施之前就用严格可靠的方法对其进行分析验证，是一个最有前途的研究方法。目前在各种电子商务协议形式化分析方法研究中，有影响的方法主要有BAN逻辑方法、Kailar逻辑方法、串空间方法、进程代数方法及基于时序逻辑的方法等。其中，时序逻辑方法能够通过建立数学模型来描述协议系统，可提供相应的模型检测工具对协议性质进行自动验证，对状态空间有限的并发协议系统分析尤为成功，已成为对电子商务协议进行形式化分析的主要工具之一。 本文主要对基于逻辑的形式化方法与模型检测技术及其在电子商务协议形式化分析中的应用进行了系统研究，重点对ATL逻辑方法及其在电子商务协议并形式化分析中的应用进行了研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术，其工作主要有以下几个方面： 1．对电子商务协议的基本理论和基本性质进行了分析和讨论，包括：安全性、保密性、完整性、可认证性、非否认性、公平性、时效性等，并对其中一些重要性质做新的定义，提出电子商务协议设计的基本准则。 2．对当前流行的基于逻辑的电子商务协议形式化分析方法进行重点研究，包括BAN逻辑、Kailar逻辑及周一卿方法。采用这些较新的形式化分析方法对几个典型协议进行分析，找出设计缺陷并提出新的公平非否认性协议。