摘要： 在电子商务领域，其协议的安全性和原子性是两个重要的问题，有必要对不断发展的协议进行分析和检验。文[3]提出了逻辑分析和进程演算相结合的技术，但这种技术在分析电子商务协议的安全性和原子性时存在一些局限性，因而本文提出了一种新的分析和检验原子性的方法。

关键词: 电子商务协议 安全性 原子性 形式化方法