电子商务协议形式化分析是电子商务研究的一个重要方面，电子商务协议是面向电子商务的密码协议，安全的电子商务协议是保证电子商务活动正常开展的基础。进行电子商务协议的形式化分析研究具有重大理论意义和现实的应用价值，是顺利开展电子商务应用的技术保障。形式化的方法是分析安全协议的主要方法。目前已经有很多研究安全协议的理论和方法，其中比较著名的有可证明安全理论、BAN类逻辑以及模型检测和定理证明的方法等。本文主要对基于逻辑的形式化方法与模型检测技术及其在电子商务协议形式化分析中的应用进行了系统研究，重点对SVO逻辑方法在电子商务协议时限性形式化分析中的应用进行了研究。总的来说，从理论到实践两个层面上研究了电子商务协议的形式化分析的相关技术。本文所做的工作、技术难点和创新之处如下：(1)首先从电子商务安全出发，对电子商务协议及其协议形式化分析的国内外研究现状进行了综述。(2)研究了BAN逻辑和其相关形式化协议分析的方法、步骤，对BAN的公理规则进行了部分扩展。同时对SVO逻辑进行了部分扩展，使该逻辑可以分析电子商务协议的时限性。(3)对模型检测工具SPIN进行了详细的介绍，通过研究Promela语言，发现该语言对时间段的模拟依然比较困难，但是通过编程技巧，可以模拟时间段的一些特性，从而模拟检测协议的时间特性。(4)利用公钥密码机制对Kerberos身份认证协议进行了改进，并利用扩展的BAN逻辑准确地描述并证明了改进后的Kerberos身份认证协议的安全性。(5)通过研究NZG协议和ISI协议，根据它们各自的优缺点，构造了一个新的基于B2C电子商务协议，使其具有了匿名性、公平性、时限性等特性。(6)运用扩展后的SVO逻辑，将该电子商务协议属性抽象化，并分析验证其是否具有时限性，证明出协议具有时限性。通过模型检测工具SPIN的模拟检测，说明新协议具有时限性。分析结果表明，对SVO逻辑的改进是有效和成功的。