随着互联网的不断发展，在世界范围内掀起了一股电子商务热潮。而网上电子支付的安全性却成为其发展的主要障碍。安全电子交易协议SET(Secure Electronic Transaction)是由ViSa和MasterCard所开发的，是为了在Internet上进行在线交易时，保证信用卡支付的安全而设计开发的一个开放规范。作者旨在研究和分析SET协议的安全机制，对形式化逻辑Kailar进行了扩充，并用该逻辑对SET协议进行了形式化分析。 本文首先对SET协议的基本结构、证书管理和交易流程进行了分析，对整个协议的安全机制进行了研究，包括协议中使用的加密算法、数据封装格式和安全性。从分析结果来看，SET协议使用的加密算法已不再安全，而且对系统的速度和交易成本有较大的影响。 然后，本文提出在SET中使用IDEA算法代替DES算法，椭圆曲线算法代替RSA算法，并对新旧算法作了比较，分析了IDEA算法和椭圆曲线密码体制的安全性基础，以及目前存在的对这两种算法的攻击。设计了一种基于椭圆曲线密码体制的认证、加密和签名方案，以代替RSA算法，使网络交易的安全性、性能和速度获得显著的提高。 最后，作者用BAN逻辑分析了X.509协议，发现了协议中存在的两个缺陷，并提出了改进的建议。同时，对Kailar逻辑进行了分析，指出了其逻辑上存在的三个主要缺陷。在此基础上，本文对Kailar逻辑进行扩充，使之不但可以分析协议的公平性，也可以用来分析电子证书、密文来源、签名密文等，并用扩充后的Kailar逻辑分析了SET协议，验证了SET协议的安全性。