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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
AT&T. FSM Library, http://www.research.att.com/sw/tools/fsm
Barret, W.A., Couch, J.D.: Compiler Construction: Theory and Practice. Science Research Associates (1979)
Billington, J.: Formal Specification of Protocols: Protocol Engineering. In: Encyclopedia of Microcomputers, pp. 299–314. Marcel Dekker, New York (1991)
Billington, J., Díaz, M., Rozenberg, G. (eds.): APN 1999. LNCS, vol. 1605. Springer, Heidelberg (1999)
Billington, J., Wilbur-Ham, M.C., Bearman, M.Y.: Automated Protocol Verification. In: Protocol Specification, Testing and Verification, V, pp. 59–70. Elsevier Science Publishers, Amsterdam (1986)
Bray, T., Paoli, J., Sperberg-McQueen, C.M., Maler, E.: Extensible Markup Language (XML) 1.0 (2nd Edn.). W3C Recommendation (October 2000)
Burdett, D.: Internet Open Trading Protocol - IOTP Version 1.0. IETF Trade Working Group (April 2000), http://www.ietf.org/rfc/rfc2801
Eastlake, D.E., Smith, C.: Internet Open Trading Protocol – HTTP Supplement. IETF Trade Working Group (September 2000), http://www.ietf.org/rfc/rfc2935
InterPay I-OTP, ftp://ftp.pothole.com/pub/ietf-trade/IETF-London/InterPay2001London.ppt
ITU. Information Technology – Open Systems Interconnection – Basic Reference Model: Conventions for the Definition of OSI Services. ITU-T Recommendation X.210 | ISO/IEC 10731 (November 1993)
Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science, vol. 1-3. Springer, Heidelberg (1997)
Mondex, http://www.mondexusa.com/
Ouyang, C., Kristensen, L.M., Billington, J.: An Improved Architectural Specification of the Internet Open Trading Protocol. In: Proceedings of 3rd Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, pp. 119–137. DAIMI PB-554, University of Aarhus (2001) ISSN 0105-8517
Ouyang, C., Kristensen, L.M., Billington, J.: Towards Modelling and Analysis of the Internet Open Trading Protocol Transactions using Coloured Petri Nets. In: Proc. of 11th Annual International Symposium of the International Council on System Engineering, 8 pages (2001)
Ouyang, C., Kristensen, L.M., Billington, J.: A Formal and Executable Specification of the Internet Open Trading Protocol. In: Bauknecht, K., Tjoa, A.M., Quirchmayr, G. (eds.) EC-Web 2002. LNCS, vol. 2455, pp. 377–387. Springer, Heidelberg (2002)
Ouyang, C., Kristensen, L.M., Billington, J.: A Formal Service Specification of the Internet Open Trading Protocol. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 352–373. Springer, Heidelberg (2002)
Hitachi SMILEs, http://www.hitachi.co.jp/Div/nfs/whats_new/smiles.html
Visa and Master Card. SET Secure Electronic Transaction Specification. Version 1.0. Vol. 1-3 (May 1997), http://www.setco.org/set_specifications.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ouyang, C., Billington, J. (2003). On Verifying the Internet Open Trading Protocol. In: Bauknecht, K., Tjoa, A.M., Quirchmayr, G. (eds) E-Commerce and Web Technologies. EC-Web 2003. Lecture Notes in Computer Science, vol 2738. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45229-4_29
Download citation
DOI: https://doi.org/10.1007/978-3-540-45229-4_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40808-6
Online ISBN: 978-3-540-45229-4
eBook Packages: Springer Book Archive