Finite-state verification of the ebXML protocol

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.