计算机网络技术飞速发展，网络化和全球化成为不可抗拒的世界潮流，电子商务成为Internet及信息技术向纵深发展的一个重要标志，是历史进步的一个里程碑。在电子商务活动中，e-Cash以极好的安全性、可靠性和匿名性，受到人们的青睐，成为一种重要的、不可替代的电子支付手段。本文针对e-Cash交易协议中原子性与匿名性之间的矛盾，以保护交易双方利益为出发点，围绕e-Cash交易协议的模型、算法、形式化验证方法等方面展开深入研究。本文主要研究内容如下： 1．根据e-Cash的交易特点，总结归纳了为保护交易双方利益，e-Cash交易协议必须满足的各种属性；同时，对e-Cash交易协议的安全技术体系进行了分析，明确了e-Cash交易协议在体系中的层次位置。 2．在交易协议安全技术体系及其逻辑层次分析的基础上，对e-Cash交易的底层安全技术展开了两方面的研究： (1)底层防火墙技术的研究与实现。基于Linux的IPChains实现用户访问控制。利用Linux内核IPChains，引入“挑战—应答”身份认证机制来实现用户的访问控制；该系统除具有透明性和一致性之外，仍具有包过滤防火墙的高效性，是一种保证电子交易安全、相对简单、实用、高效的防火墙访问控制系统； (2)基于VPN的AAA管理系统的研究。根据IPSec为隧道协议的虚拟专用网络系统的特点，通过制订了一套完整的AAA管理通信协议来实现认证、授权、记账三方面的功能，并且采用分散管理的机制和策略化网络连接思想，从而提高了系统灵活性，是更为方便、灵活、高效的用户管理系统。 通过对底层安全技术的研究，为e-Cash交易协议提供了底层网络服务平台，为后续基于e-Cash交易协议的深入研究奠定基础，以便更好地进行核心问题的研究。 3．通过对e-Cash协议属性及多个e-Cash交易协议的研究分析，针对e-Cash交易协议的匿名性和原子性之间存在的矛盾，以及目前对于该矛盾的解决方案中，对协议核心属性讨论层次不够清晰，难以直接确定协议属性本质的问题，基于文献[87]提出的电子商务系统框架的基础上，利用Linear-Time Temporal逻辑，提出并建立了离线可信第三方匿名原子的电子现金交易协议模型，并对协议模型中的原子性进行详细分析证明。大连理工大学博士学位论文 4.在RSA可转换不可否认签名方案的基础上，提出了交互确认协议—ICSP协议，并证明该协议安全、有效。同时，利用扩展CEMBS算法和ICSP交互确认协议，基于Brands电子现金方案，设计并提出了离线可信第三方匿名原子e一Cash交易协议。对所设计协议的原子性、匿名性、终止性、不可否认性、安全有效性进行了分析证明，并与同类典型协议在效率、存贮量、交易时限和终止性等方面进行比较，证明了设计协议的高效性。 5.基于SVO逻辑，提出了一种验证电子商务交易协议的新形式化逻辑验证方法。通过对两个经典的电子商务交易协议的实例分析，发现了SVO逻辑在分析电子商务交易协议中存在的局限与不足。通过引入交易协议的动态性概念，对原有SVO逻辑分析框架进行扩展，提出了一种更适合于分析电子商务交易协议的新形式化逻辑验证方法。新方法对于协议的分析具有不需人为引入初始化假设，仅依赖协议的运行环境的特点，是一个更为严密的形式化分析方法;同时，新方法不仅可以静态验证协议的不可否认性，还能够动态验证协议的原子性。并利用新方法对多个经典电子商务协议进行实例分析，验证了新方法的正确性、有效性。同时，使用新方法对本文所设计的e一Cash交易协议的原子性和不可否认性进行了验证。