Abstract: The simplified model of payment process of the SET protocol is used to build up its formal model and finite state machine model，as well as CTL formulations of the security properties are presented.Under the assumption of the network environment being controlled by intruder，the symbolic model checking ware（SMV） is applied for analyzing the authentication，confidentiality and integrity，attacks are found.Then，the influence of attacks is discussed.Finally，the protocol model is optimized.The result of analysis and checking indicates the importance of dual signature on SET protocol.

摘要： 在以Lu&Smolka对SET协议支付过程的简化模型为研究对象的情况下，进行形式化建模和有限状态机模型。同时应用CTL对相应的安全性质进行形式描述，并在网络环境被入侵者控制的假设下，利用SMV分析了协议的认证性、保密性和完整性，发现攻击并对该攻击所产生的影响进行了讨论。最后修改其协议模型对改进后的协议进行分析和检验，说明了SET协议独具特色的双重签名在整个协议运行中至关重要。