استاندارد و تایید عادلانه ارز و ظرفیت اتمی در معاملات تجارت الکترونیک

Electronic commerce can be defined as the conduct of commerce in goods and services, with the assistance of telecommunications and telecommunications-based tools. The economic growth potential of e-commerce is extraordinary—but so are the challenges that lie on the path toward success. One of the more pressing challenges is how to ensure the integrity and reliability of the transaction process: key aspects being fair-exchange and atomicity assurance. This paper delineates an extended fair-exchange standard, which includes atomicity assurance, intended for a wide audience including e-commerce designers, managers, users, and auditors. We demonstrate how such a standard prevents or mitigates important e-commerce concerns. To bridge theory with practice, we illustrate how the application of model checking can be used to verify the correctness of the implementation of e-commerce protocols to prevent the failure of such protocols when unforeseen circumstances occur.

Development of protocols, or standards, for the exchange of electronic information between transacting parties has expanded from proprietary arrangements for each set of transacting parties (e.g., early EDI) to proprietary standards for communities of transacting parties (e.g., CommerceOne) to menus of public standards from which transacting parties choose (e.g., UDDI and SOAP). Notwithstanding their contributions to facilitating electronic exchanges, these standards focus primarily on facilitating the transaction process. In other words, current practice focuses on establishing methods to complete a transaction. Zhang et al. [1] observe that although this is an essential requirement for engaging in e-commerce, it is generally insufficient to warrant the integrity and reliability of the transaction process under all possible contingencies. To prevent or mitigate these concerns, Zhou and Gollman [2] have identified conditions that e-commerce protocols must satisfy, which include: 1. Standards should ensure fair-exchange. 2. Standards should not require manual dispute resolution in case of unfair behavior by one party. 3. Standards should provide parties with assurance that the goods or assets they are about to receive are the correct ones, are undamaged, and are in the right quantity. 4. Standards should enable involvement of a trusted third party (TTP). 5. All transaction operations should be completed, or no operations should be completed. Items 1, 2, 3, and 4 are characteristics of a fair-exchange standard whereas item 5 is a characteristic of atomicity. Fair-exchange ensures that the two parties obtain their respective items without allowing either party to gain an advantage by unexpectedly leaving the transaction or otherwise misbehaving [3]. Atomicity enables the linking of multiple operations associated with different parties to an e-commerce transaction such that either all necessary operations are executed or none of them are [4]. Although existing e-commerce protocols may be able to protect the integrity and reliability of e-commerce transactions in most situations, guaranteeing integrity and reliability under all circumstances is exceptionally difficult and complex. A familiar parallel is found in the development of operating system software. Software designers focus on creating a functional operating system that properly performs its operations and is robust to all preconceived events. Yet, as evident from the frequent release of operating system patches, unforeseen events arise which require additional “features” to be added. Similarly, e-commerce protocols may respond well to preconceived events. However e-commerce protocols (like operating systems) are not consistently tested for robustness to unforeseen patterns of events. Assuring correct processing under all circumstances requires extensive analysis of the standards used in the transaction process. Methods such as theorem proving, simulation, and model checking have been proposed and used in performing portions of such an analysis. Yet, analyzing an e-commerce protocol alone is insufficient to assure correct processing—the standard must also be applied. For example, a company may adopt a standard that is conceptually robust to issues of integrity and reliability, but operational details may be introduced that result in unanticipated transaction failures. The foundations from which this paper is constructed were first developed by Ray and Ray [3] and [5] and Ray et al. [6]. Our contribution is an integration of model checking with fair-exchange theory to yield a robust e-commerce protocol that integrates fair-exchange with assurance of transaction atomicity. This is presented with detailed examples to enhance accessibility to a wider audience. The paper proceeds as follows: First we describe the concepts of fair-exchange and atomicity, including three types of atomicity critical to electronic commerce. Second, we address the implementation of a fair-exchange standard for electronic transactions. Third, we briefly motivate the use of model checking to verify that an implementation satisfies user specifications—in this case atomicities. Fourth, we provide an outline of an application, which is then used to demonstrate the use of model checking. We then discuss the results and explain how the extended standard mitigates the concerns identified early in the paper. Finally, we offer some concluding observations.

Implementing e-commerce systems using existing e-commerce protocols is highly complex. It is further complicated by distributed processing, parallelism, concurrency, communication uncertainties, and continuous operations. Assuring fair-exchange and atomicity in this environment requires a designer to analyze potential interactions among the trading parties along with the dynamics of their technological environments. This results in a very large state space of possible interactions among trading parties. The analysis of this state space is virtually impossible for humans to accomplish. Model checking can assist designers and auditors in evaluating this state space and assuring fair-exchange and atomicity. We have explained the concepts involved in implementing an extended fair-exchange standard that involves atomicity, and we have shown how such a standard can be implemented and verified using model checking. As new standards are developed or as existing standards are modified, developers should address the issues of fair-exchange and atomicity. In addition, as businesses implement their e-business models, they should address whether their implementation is robust to fair-exchange and atomicity. Model checking can provide a rigorous means of assuring fair-exchange and atomicity for either of these scenarios.