随着电子商务的不断发展，电子商务的安全一直备受人们关注。SET协议作为电子商务中的关键协议，其安全性的重要性不言而喻。形式化方法作为重要的协议安全性分析方法，以其严密性和准确性的特点已成为检验网络安全协议安全性的重要途径。模型检测是形式化方法中非常重要的一种方法，已成功地运用于网络协议的安全性验证。由于协议的安全性问题十分微妙，有些本身并不复杂的协议的安全漏洞在协议使用很长时间后才被发现。进而，分析和研究SET协议的安全性，找出其存在的安全漏洞或者证明其为安全的，对协议的进一步发展及应用有着非常重要的意义。本文主要运用模型检测方法对SET协议进行形式化分析与验证。首先对协议的形式化分析方法、模型检测技术、SPIN验证工具、Promela语言、线性时态逻辑LTL等相关理论进行了介绍；其次对SET协议的工作原理及其支付过程的各个阶段进行了形式化描述和分析，针对该协议的支付过程采用了基于Lu&Smolka的SET协议简化模型，并运用Promela语言对该协议进行形式化建模，在网络环境被入侵者控制的假设下，运用SPIN发现了攻击；采用atomic、d_step、偏序规约及Bit-state hashing等优化技术来缓解状态空间爆炸、减少存储空间，从而提高验证效率；最后针对协议存在的漏洞对协议进行改进，并再次使用模型检测工具SPIN验证了改进后的SET协议的正确性。