目前,电子商务中主要采用的安全协议有:安全套接层协议(SSL:SecuritySocket Layer)协议和安全电子交易协议(SET:Secure ElectronicTransaction)。SET协议在Internet购物环境中提供了消费者、商家和银行之间的认证,确保了交易数据的安全性、完整性、可靠性和交易的不可否认性。目前,SET协议已获得IETF标准认可,已成为事实上的标准。但是,到目前为止SET协议并未吸引足够的商家和消费者,并没有得到广泛的应用,其原因在于SET协议本身比较复杂,处理速度慢,完成一个SET交易过程需要较长时间;SET协议只保证了钱原子性,并不满足发送原子性和商品原子性,没有解决交易后证据的生成和保留问题;SET协议没有说明收单银行给在线商店付款前,是否必须收到消费者的货物接受证书,因此,在线商店提供的货物不符合质量标准,消费者提出异议,责任由谁来负。BAN逻辑和Kailar逻辑是常见的电子商务协议形式化分析方法,但是它们只能分析电子商务协议的有限性质,不能分析电子商务协议的可追究性,并且在遇到重放攻击时BAN逻辑和Kailar逻辑不能正确分析主体的责任性。本文对SET协议进行了全面的分析研究,对SET协议交易模型进行了改进,提高了SET协议交易效率,对SET协议存在的各种问题提出相应的改进方案,完善了SET协议。同时,对Non-monotonic Dynamic逻辑进行了研究,结合Kailar逻辑的优点,利用一种新的用于分析电子商务协议的形式化逻辑语言对改进后的SET协议进行逻辑抽象,对改进后的SET协议进行了完全的形式化分析,证明了其安全性。