电子商务协议的安全性、原子性、不可否认性等性质的验证的方法一直制约着电子商务的发展。形式化分析技术可使协议设计者通过系统分析将注意力集中于接口、系统环境的假设、在不同条件下系统的状态、条件不满足时出现的情况以及系统不变的属性,并通过系统验证,提供协议必要的安全保证。目前,国内外形式化研究安全协议主要有基于知识与信念推理的模态逻辑方法,基于定理证明的方法和基于攻击的结构性方法三种。电子商务协议作为安全协议的一部分,这些方法在电子商务协议中同样有效。本论文应用形式化方法对电子商务协议进行分析,工作如下;1.概述了电子商务协议的发展过程以及在此发展过程中运用的加密方式和形式化方法。2.分析了电子商务协议的安全性质,如匿名性、原子性、不可否认性等,并给出了实例分析。3.在对电子商务协议安全性质全面分析的基础上,设计了一个安全的电子商务协议。该协议满足钱原子性、商品原子性以及不可否认性,最后对协议进行了详细分析。