安全性和可靠性是电子商务交易协议安全领域最重要的部分。同时支付宝作为国内第三方支付平台代表之一,其安全性对国内电子商务安全的影响较大。在大量阅读国内外交易协议和形式化验证文献的基础上,本文通过接口分析、数据包采样分析等方式确定支付宝交易的流程,并以此为基础利用有限自动机理论对支付宝交易协议进行形式化验证,在分析验证过程中针对支付宝交易协议存在的买家隐私暴露问题提出了改进方案和框架。(1).本文提出了一种基于有限自动机理论对交易协议进行形式化分析和验证的框架,并以支付宝交易协议的完整流程为例进行安全分析和验证。(2).在深入研究支付宝交易协议的基础上,分析发现该交易协议中存在隐私信息过度暴露的问题,并提出了一种保护买家隐私的网上购物解决方案。该方案即能有效解决买家隐私泄露问题,又能解决电子商务中信息监管的问题。(3).本文还对改进型交易协议的协议安全属性规范进行了分析。