On verifying the internet open trading protocol

Abstract

The Internet Open Trading Protocol (IOTP) is designed to support a set of electronic transactions that capture common trading activities. The protocol provides reliable trading transaction services that are payment-system independent. To verify IOTP, we use a protocol verification methodology that compares IOTP’s service and protocol languages. The service language is generated from the service model specifying only the external behaviour of IOTP, whereas the protocol language is obtained from the protocol model by hiding internal operations of IOTP. Comparing these two languages indicates whether IOTP formally conforms to its service. The initial verification results show that IOTP transactions that are successful, error-free and independent of each other, implement a subset of the service language. We conclude that this subset is a valid implementation of the service and is due to the way IOTP combines messages in some circumstances.