Skip to main content
SpringerLink
Log in

Formal Analysis of the Internet Open Trading Protocol

  • Conference paper
Applying Formal Methods: Testing, Performance, and M/E-Commerce (FORTE 2004)

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

Abstract

The Internet Open Trading Protocol (IOTP) is an electronic commerce (e-commerce) protocol developed by the Internet Engineering Task Force (IETF) to support online trading activities. The core of IOTP is a set of financial transactions and therefore it is vitally important that the protocol operates correctly. An informal specification of IOTP is published as Request For Comments (RFC) 2801. We have applied the formal method of Coloured Petri Nets (CPNs) to obtain a formal specification of IOTP. Based on the IOTP CPN specification, this paper presents a detailed investigation of a set of behavioural properties of IOTP using state space techniques. The analysis reveals deficiencies in the termination of IOTP transactions, demonstrating the benefit of applying formal methods to the specification and verification of e-commerce protocols.

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

Access this chapter

Log in via an institution
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. Babich, F., Deotto, L.: Formal methods for the specification and analysis of communication protocols. IEEE Communication Surveys 4(1), 2–20 (2002)

    Article  Google Scholar 

  2. Billington, J., Gallasch, G.E., Han, B.: A Coloured Petri Net approach to protocol verification. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, 80 pages. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Birch, D.: Shopping Protocols - Buying online is more than just paying. Journal. of Internet Banking and Commerce 3(1) (January 1998), Available via: http://www.arraydev.com/commerce/JIBC/9801-9.htm

  4. Burdett, D.: Internet Open Trading Protocol - IOTP Version 1.0. IETF RFC 2801, Available via (April 2000), http://www.ietf.org/rfc/rfc2801

  5. Burdett, D., Eastlake, D.E., Goncalves, M.: Internet Open Trading Protocol. McGraw-Hill, New York (2000)

    Book  Google Scholar 

  6. Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)

    Article  Google Scholar 

  7. InterPay I-OTP (August 2001), http://www.ietf.org/proceedings/01aug/slides/trade-1/index.html

  8. Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. In: Nonmonotonic Logics, 2nd edn. Monographs in Theoretical Computer Science, vol. 1, Springer, Berlin (1997)

    Google Scholar 

  9. Jensen, K.: Basic Concepts, Analysis Methods and Practical Use. In: Analysis Methods, 2nd edn. Monographs in Theoretical Computer Science, vol. 2, Springer, Berlin (1997)

    Google Scholar 

  10. Kessler, G.C., Pritsky, N.T.: Payment protocols: Cache on demand. Information Security Magazine (October 2000), Available via http://www.infosecuritymag.com/articles/october00/features2.shtml

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

  12. Design/CPN Online, http://www.daimi.au.dk/designCPN

  13. Ouyang, C., Billington, J.: On verifying the Internet Open Trading Protocol. In: Bauknecht, K., Tjoa, A.M., Quirchmayr, G. (eds.) EC-Web 2003. LNCS, vol. 2738, pp. 292–302. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  14. Ouyang, C., Billington, J.: An improved formal specification of the Internet Open Trading Protocol. In: Proceedings of the 2004 ACM Symposium on Applied Computing (SAC 2004), Nicosia, Cyprus, March 14-17, pp. 779–783. ACM Press, New York (2004)

    Chapter  Google Scholar 

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

  16. Papa, M., Bremer, O., Hale, J., Shenoi, S.: Formal analysis of e-commerce protocols. IEICE Transactions on Information and Systems E84-D(10), 1313–1323 (2001)

    MATH  Google Scholar 

  17. Standard SMart Card Integrated SettLEment System Project SMILE Project (April 1999), http://www.ietf.org/proceedings/99mar/slides/trade-smile-99mar

  18. Visa and MasterCard. SET Secure Electronic Transaction Specification. Vol. 1-3 (May 1997), Available via http://www.setco.org/setspecifications.html

Download references

Author information

Authors and Affiliations

  1. Computer Systems Engineering Centre, School of Electrical and Information Engineering, University of South Australia, SA, 5095, Australia

    Chun Ouyang & Jonathan Billington

Authors
  1. Chun Ouyang
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jonathan Billington
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. Sistemas Informáticos y Programación Facultad de Informática, Universidad Complutense de Madrid, 28040,, Madrid, Spain

    Manuel Núñez

  2. CIT, Zayed University, Dubai, United Arab Emirates, United Arab Emirates

    Zakaria Maamar

  3. Dept. de Sistemas Informáticos Escuela Politécnica Superior, Universidad Castilla-La Mancha, 02071, Albacete, Spain

    Fernando L. Pelayo

  4. Business Informatics and Systems Engineering, University of Augsburg, Universitätsstraße 16, 86135, Augsburg, Germany

    Key Pousttchi

  5. Dept. Sistemas Informáticos y Computación, Facultad de Informática, Universidad Complutense de Madrid, Madrid, Spain

    Fernando Rubio

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ouyang, C., Billington, J. (2004). Formal Analysis of the Internet Open Trading Protocol. In: Núñez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds) Applying Formal Methods: Testing, Performance, and M/E-Commerce. FORTE 2004. Lecture Notes in Computer Science, vol 3236. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30233-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-30233-9_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-23169-1

  • Online ISBN: 978-3-540-30233-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation