电子商务安全协议及其非单调动态逻辑验证

该文介绍了SET(secure electronic transactions)的付费业务流程,对NDL(non-monotomic dynamic logic)的逻辑框架进行了扩展,即针对SET协议,增加了新的公理,重新给出积累规则的定义.在此基础上,用对SET中的几个重要的范例进行的逻辑验证,说明了NDL在验证电子商务协议上的重要性,并初步提出了积累规则中需要进一步研究的问题.     

SET证书申请协议在SPV下的自动化验证及改进

基于实例化空间逻辑理论,使用知识推理方法,在SPV(Security Protocol Verifier)下对完整SET证书申请协议的秘密性、认证性等安全性质进行了完全自动化证明,并对协议进行了改进.SPV调用工业级SAT求解器,能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范.应用一个逻辑或工具对协议进行验证首先必须对该协议进行简化,而SET协议作为当前最复杂的工业级协议,其原始文档有上千页,因此简化过程相当困难,相关研究较少,已有的一些简化模型也不够完整.因此,文章针对SET证书申请协议,给出了比以往更贴近原协议的简化模型,并详细阐述了该模型在SPV下的形式化描述及验证过程、验证结果,分析了由于协议不满足某些认知规范所带来的安全隐患,从而对协议进行改进,最后证明了改进后协议的有效性.该工作也充分说明了SPV足以处理复杂的工业级协议.     

移动电子商务的电子支付模型研究

电子支付技术是电子商务中的核心技术，也是目前制约电子商务发展的一个根本性问题，移动电子商务也不例外，文章对移动电子商务中的支付体系进行了深入的探讨，提出了适合移动电子商务发展的M－SET移动支付模型，并用BAN逻辑对其安全性进行了验证。     

SET协议在网上支付中的应用研究

通过对原SET(Secure Electronic Transaction)协议的安全标准进行分析,指出SET协议在网上支付应用中存在的流程问题和密码技术的安全隐患.针对这些缺陷和不足,给出了SET协议的改进方案,改进后的SET协议通过引进第三方支付平台和增加的加密对整个数据传输的过程进行了重组,同时,增加的部分环节的加密技术改进了数据传输过程中的部分消息源认证问题.     

基于小系统理论的简化SET协议

基于Lu & Smolka的SET协议支付过程简化模型,在小系统理论的基础上,运用Promela语言对协议进行形式化建模,采用线性时态逻辑LTL公式对协议的认证性进行形式化描述。在网络环境被入侵者控制的假设下,运用SPIN发现攻击;采用atomic和Bit-state hashing等优化策略,降低模型检测的复杂性,提高验证效率;最后针对协议存在的漏洞提出协议改进方案。     

小额交易中SET协议的优化及SPIN验证的研究

作为电子商务的重要组成部分,基于Internet的电子交易受到了广泛的关注。SET交易过程十分复杂,在完成一次SET协议交易过程中,需验证电子证书9次,验证数字签名6次,传递证书7次,进行签名5次,4次对称加密和非对称加密。本文选取SET协议的核心部分：购买请求、支付认证和获得付款3个子协议过程作为研究分析对象,针对不同数额的交易进行分级,针对小额的交易过程进行协议的优化,对SET进行SPIN模型检测,并根据分析模拟与验证的结果对SET进行改进。     

SET协议的安全性分析及改进

对SET协议中电子交易信息的机密性、身份认证、数据完整性进行了详细的阐述,并对“不可否认性”验证和国家安全部门强制介入的情况提出了解决的措施,还分析了SET协议中电子交易“时效性”的问题。     

一种SCADE同步语言程序安全属性自动验证工具

安全关键领域的反应系统大都采用同步语言开发,然而,学术界尚不存在SCADE同步语言程序的形式化验证工具,为此,本文提出了一种自动验证SCADE同步语言程序安全属性的方法.首先使用无量词一阶逻辑公式对SCADE同步语言程序的行为进行建模,可将SCADE同步语言程序的安全属性的验证问题转化为无量词一阶逻辑公式的可满足性问题;然后采用先进的可满足性模理论求解器对其可满足性进行求解.本方法旨在实现对SCADE同步语言程序进行自动地、直接地验证,以填补SCADE同步语言程序验证领域的技术空白.此外,本文对所提方法进行了代码实现,并通过实验验证了所提方法的有效性.     

一种新的时段演算及其验证

在Pandya提出的CTL*[DC]逻辑的基础上,对其语法和语义进行扩展,并对路径长度进行限制,定义了一个新的逻辑CTL*[k-QDDC],它可应用于实时系统的描述和验证.给出了在Kripke结构中直接验证CTL*[k-QDDC]逻辑公式在某状态是否成真的基本算法.在某些假设下,也证明了CTL*[k-QDDC]中的某个逻辑运算符的验证问题是NP完全的,这就说明CTL*[k-QDDC]的验证问题至少是NP难的.     

面向无穷数据的形式模型综述

无穷数据广泛存在于计算机程序和数据库系统中.受到形式验证与数据库两方面的应用需求的推动,面向无穷数据的形式模型已经成为理论计算机科学的一个研究热点.本论文对面向无穷数据的形式模型(逻辑与自动机)进行了相对全面详细的总结.本论文主要按照不同自动机模型对无穷数据的处理方式来组织,主要关注相关判定问题,即自动机的非空性问题、语言包含问题,以及逻辑的可满足性问题,的可判定性与复杂性.     

一个公平、有效的安全电子交易协议

SET（安全电子交易）协议是由MasterCard和VISA制定的，基于信用卡的安全支付协议。在SET协议基础上提出了一种有效公平的安全电子交易协议（SET－1），该协议不仅保持了SET原有安全和有效的特性，而且实现了交易有效证据的生成和保存，从而保证了交易的公平性，同时还引入交易状态机制。最后，讨论该协议的安全性、有效性和公平性。     

SET协议系统缺陷及其改进方案

电子商务的流行与接受主要取决于下述属性:安全、原子、匿名和不可否认性。文章对现在流行的安全电子交易SET标准进行分析,指出SET协议存在不满足数字商品交易的原子性以及确认发送原子性等缺陷。并在原有SET基础上对其协议流程进行改进,使其不仅具有交易原子性,而且还使用交易双方具有不可否认性以及公平交易等特点。     

A flaw in the electronic commerce protocol SET

The Secure Electronic Transaction (SET) protocol has been developed by the major credit card companies in association with some of the top software corporations to secure e-commerce transactions. This paper recalls the basics of the SET protocol and presents a new flaw: a dishonest client may purchase goods from an honest merchant (with the help of another merchant) for which he does not pay. Fortunately, by checking his balance sheet, the merchant may trace with the help of his bank the client and his accomplice. We also propose a modification to fix the flaw.     

基于高级SET协议的电子商务安全*

在充分分析安全电子交易的前提下,针对目前流行的SET标准协议进行分析,指出了SET协议在交易过程中的各种缺陷,进而提出了SSET协议,并对SSET协议的工作流程进行详尽阐述。SSET协议增强了原有SET协议的安全性和不可否认性,满足了交易原子性、隐私保护性,并提出了信用等级制度和纠纷仲裁机制,完善了电子交易的整个过程,切实保护了各方利益。     

用于灾难恢复的远程备份系统的模型与算法

本文系统深入地介绍了现有远程备份系统的体系结构、模型和算法,讨论了每种模型和算法的适应范围及优点,分析了存在的缺陷和问题。在此基础上,提出了优化o2-safe 算法。该算法在保证系统完整性和一致性的前提下,充分挖掘事务间的并发执行性,增加了事务处理的吞吐量。最后,讨论了用于灾难恢复的远程备份技术的发展趋势。     

SET协议关键事务的XML Schema定义

安全电子交易SET是一个用于保护Internet上信用卡交易的加密与安全规约,它定义了多种事务类型,其中最重要的三种事务分别为购买请求事务、支付授权事务和支付获取事务,要求在理解SET协议关键事务的基础上,为了实现数据的互操作要求,采用XML作为消息的载体,设计与SET协议关键事务相关的XML Schema定义,要求能够完整准确地表达消息的各种要素.     

一种SET协议中持卡者端的实现策略

SET（Secure Electronic Transaction，安全电子交易协议）是由Visa和MasterCard公司于1997年5月联合开发的一个为了在Internet上进行在线交易时保证信用卡支付安全的一个开放的规范。目前，绝大多数的SET协议持卡者端的实现是一个称为电子钱包的“胖”客户端，用户使用起来并不是很方便，该文所描述的采用服务器钱包的策略，即将原来的电子钱包分为电子钱包服务器与电子钱包客户端，简化了用户对电子钱包的使用，促进了基于SET协议的电子商务应用解决方案的推广。     

Verifying the SET Purchase Protocols

SET (Secure Electronic Transaction) is a suite of protocols proposed by a consortium of credit card companies and software corporations to secure e-commerce transactions. The Purchase part of the suite is intended to guarantee the integrity and authenticity of the payment transaction while keeping the Cardholder's account details secret from the Merchant and his choice of goods secret from the Bank. This paper details the first verification results for the complete Purchase protocols of SET. Using Isabelle and the inductive method, we show that their primary goal is indeed met. However, a lack of explicitness in the dual signature makes some agreement properties fail: it is impossible to prove that the Cardholder meant to send his credit card details to the very payment gateway that receives them. A major effort in the verification went into digesting the SET documentation to produce a realistic model. The protocol's complexity and size make verification difficult, compared with other protocols. However, our effort has yielded significant insights.