安全的电子商务协议是保证电子商务活动正常开展的基础。一个貌似安全的协议往往存在安全上的漏洞。模型检测是一种常见的形式化分析方法，在验证电子商务协议时，它的逻辑推理能力比较弱。此外，随着网络的大规模应用，需要分析安全的电子商务协议在不可靠环境下并发运行时是否仍然保持安全性。本文主要结果如下： 1．基于消息转换的验证模型。定义了一个扩展的有限状态自动机、一些新的逻辑转换规则，并给出了详细的分析步骤。用扩展的FSA根据消息为协议建模，不仅可动态显示各个参与者并发执行协议的过程，而且增强了自动机的逻辑分析能力。利用该方法分析匿名原子交易协议，可知当交易主体诚实时，该协议满足可追究性、公平性、原子性等；对协议模型抽象后，借助模型检测工具UPPAAL验证了协议的活性。 2．基于动作转换的验证模型。定义了一个信任矩阵和一个动作集合，并将它们和逻辑规则一起引入有限状态自动机为协议参与者建模。信任矩阵形式化了协议参与者之间的信任关系，从而无需初始化假设；动作集合将加密、签名等动作明确地表示出来，从而在规范协议时无需理想化过程。利用该方法分析匿名原子交易协议，可知当交易主体不诚实时，该协议不满足可追究性；通过搜索参与者进程的模型，找到了性质不满足的原因，从而对原协议进行了修改；对修改后的协议进一步分析，发现其满足可追究性、公平性、原子性等。 3．用模型检测方法分析了不可靠环境下协议的安全性质。验证结果表明，一个安全的电子商务协议在不可靠环境下由多对参与者同时执行时，有可能不再满足安全性质；当安全性质违背时，可借助模型检测工具(本文用模型检测工具UPPAAL)生成的消息序列对协议进行改进。