Skip to main content

On Verifying the Internet Open Trading Protocol

  • Conference paper
Book cover E-Commerce and Web Technologies (EC-Web 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2738))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. AT&T. FSM Library, http://www.research.att.com/sw/tools/fsm

  2. Barret, W.A., Couch, J.D.: Compiler Construction: Theory and Practice. Science Research Associates (1979)

    Google Scholar 

  3. Billington, J.: Formal Specification of Protocols: Protocol Engineering. In: Encyclopedia of Microcomputers, pp. 299–314. Marcel Dekker, New York (1991)

    Google Scholar 

  4. Billington, J., Díaz, M., Rozenberg, G. (eds.): APN 1999. LNCS, vol. 1605. Springer, Heidelberg (1999)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. Bray, T., Paoli, J., Sperberg-McQueen, C.M., Maler, E.: Extensible Markup Language (XML) 1.0 (2nd Edn.). W3C Recommendation (October 2000)

    Google Scholar 

  7. Burdett, D.: Internet Open Trading Protocol - IOTP Version 1.0. IETF Trade Working Group (April 2000), http://www.ietf.org/rfc/rfc2801

  8. Eastlake, D.E., Smith, C.: Internet Open Trading Protocol – HTTP Supplement. IETF Trade Working Group (September 2000), http://www.ietf.org/rfc/rfc2935

  9. InterPay I-OTP, ftp://ftp.pothole.com/pub/ietf-trade/IETF-London/InterPay2001London.ppt

  10. 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)

    Google Scholar 

  11. Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science, vol. 1-3. Springer, Heidelberg (1997)

    MATH  Google Scholar 

  12. Mondex, http://www.mondexusa.com/

  13. 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

    Google Scholar 

  14. 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)

    Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Hitachi SMILEs, http://www.hitachi.co.jp/Div/nfs/whats_new/smiles.html

  18. Visa and Master Card. SET Secure Electronic Transaction Specification. Version 1.0. Vol. 1-3 (May 1997), http://www.setco.org/set_specifications.html

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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

Publish with us

Policies and ethics