摘要：随着网络的大规模应用,电子商务协议的运行环境越来越不可靠。本文用模型检测的方法分析了不可靠环境下电子商务协议的安全性质。结果表明：安全的电子商务协议在不可靠环境下运行时有可能不再保持安全性质。当安全性质违背时,借助由自动验证工具UPPAAL生成的消息序列查找原因并对协议进行修改。经验证,修改后的协议在不可靠的环境下保持安全性质。

关键词：电子商务协议 不可靠环境 模型检测 原子性 uppaal 

单位：郑州大学理论计算机研究所; 河南郑州450052; 北京航空航天大学计算机学院; 北京100083