Finite-state verification of the ebXML protocol

作者:

Highlights:

摘要

In the past few years, electronic commerce has rapidly spread through the Internet or private networks. Such a rapid development has required a standardization process since heterogeneous systems from multiple companies need to interoperate. A common problem in the area of business to business is that interoperability requires robust communication protocols.Emerging standards, such as ebXML [ebXML, ebxml specifications. Available from: ], allow the exchange of goods and services through the Internet, thus requiring a robust structure. In this paper we analyze the ebXML standard, in order to formally verify its specifications and to ensure secure transactions in a B2B environment. Analysis is conducted through a formal method, model checking that determines whether a system model satisfies certain specifications under all circumstances. A model checker allowed to automatically check the model against the properties. The approach allowed to highlight some weakness of the protocol mainly due to the lack of a clear and complete set of specifications. Solutions have been proposed to solve the weakness of the protocol in the development of an e-commerce system.

论文关键词:Model checking,ebXML,Formal verification,Business transactions

论文评审过程:Received 23 October 2004, Revised 6 September 2005, Accepted 15 September 2005, Available online 20 March 2006.

论文官网地址:https://doi.org/10.1016/j.elerap.2005.09.002