随着信息网络技术的发展,电子商务已成为Internet和信息技术向纵深发展的重要标志,同时,电子商务的安全性问题也日益突出,受到广大学者和工程技术人员的关注。电子商务安全协议是保障电子商务顺利应用与发展的关键技术。一般安全协议的安全属性通常只包括认证性、保密性和完整性,而电子商务安全协议除了包括上述属性之外,还包括非否认性、可追究性、公平性、原子性及匿名性等安全属性,因此,电子商务安全协议的设计与分析更为复杂。实践表明,即使是精心设计的协议往往也存在安全漏洞,而且使用非形式的分析方法难以发现这些漏洞。使用形式化分析方法对电子商务安全协议进行严格分析,不仅能够发现协议存在的安全漏洞和缺陷,而且其分析结果还可以用于指导电子商务安全协议的设计,弥补现有协议中的潜在问题。因此,对电子商务安全协议及其形式化分析方法研究具有重要的理论意义和现实应用价值。本文主要研究电子商务安全协议的设计与逻辑分析方法,研究内容包括以下方面：1.深入研究了典型的电子商务安全协议逻辑分析方法,指出了它们的优点与不足。使用SVO逻辑、卿-逻辑等协议逻辑分析方法,研究分析了两种常用典型电子商务协议,发现了它们存在的安全缺陷,并提出了改进协议。使用SVO逻辑分析YAHALOM协议,发现其不能抵抗重放和假冒攻击。通过修改消息格式、增加握手消息,提出了一种改进协议。分析表明,改进的协议能够实现强身份认证和密钥协商目标。针对可认证的邮件传递协议CMP1存在的缺陷,提出了改进方案,通过引入密码原语——加密Hash函数,保护了邮件消息的机密性；使用拓展的卿-逻辑分析了改进CMP1协议的安全目标。2.针对典型的电子商务安全协议逻辑分析方法存在的以下问题：安全属性分析存在局限性,缺乏形式化语义,对混合密码原语的处理能力不强,提出了一种新的逻辑分析方法新逻辑能够分析电子商务安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。定义了新逻辑的逻辑构件、公理和推理规则,引入串空间模型,描述了新逻辑所含逻辑构件的串空间语义,应用串空间模型证明了新逻辑主要推理规则的正确性。以匿名电子现金支付协议作为分析实例,证明了新逻辑方法的有效性。分析找出了该协议的安全漏洞和缺陷：不满足商家的非否认性、密钥保密性、可追究性、公平性以及原子性,客户面临商家恶意欺骗的潜在威胁。3.针对典型电子商务安全协议存在的安全目标单一,不能满足日益增加的安全需求等问题,提出了一种能够满足多种安全属性的复合型电子商务安全协议,该协议包含认证子协议和支付子协议两部分。认证子协议基于令牌概念实现了高效认证,分析表明,该协议不仅能够防止攻击者假冒交易主体,能够抵抗重放攻击和拒绝服务攻击,而且该协议交互次数少,无需数字签名,能够实现在“第一时间”对主要交易主体的身份认证,并高效产生会话密钥。改进匿名电子现金支付协议,提出了支付子协议,引入电子证书证明交易主体的身份,确保协议非否认性的实现；借助可信方传递付款收据,避免交易主体不诚实所导致的公平性缺失；引入FTP传输方式传送电子货币和付款收据,确保实现可追究性与公平性,进一步增强协议的鲁棒性。使用本文提出的新逻辑对该协议进行形式化验证,结果表明该协议能够满足认证性、密钥保密性、非否认性、公平性、可追究性以及原子性等安全属性。4.综合上述研究内容,在系统归纳一般安全协议设计准则的基础上,系统概括了已知电子商务安全协议的安全需求,提出了电子商务安全协议的设计准则,为规范工业化标准电子商务安全协议设计提供了可借鉴的参考,对电子商务协议设计与应用具有指导作用。应用上述设计准则分析并重新设计了一种典型微支付协议。微支付协议是电子商务的一种典型应用,微支付系统设计与实现需要同时考虑安全与效率两个方面。对基于传统Hash链的微支付协议NMP进行研究,发现其存在以下安全问题：不能防止用户恶意透支,没有考虑协议执行的时限性。此外,由于传统Hash链的使用存在长度限制,新Hash链验证锚的更新操作繁琐且涉及安全传递问题,所以在一定程度上影响了基于传统Hash链的微支付协议的效率和安全性。针对上述问题,基于可自更新Hash链机制,提出了一种新的微支付协议,与NMP协议相比,新协议不仅有效地解决了后者存在的上述问题,而且提高了支付效率,具有更好的公平性。分析结果表明,新协议在存储和通信载荷方面较NMP协议仅增加80 byte,但在10000份额交易下,新协议节点平均计算效率是NMP协议的125倍。