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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Babich, F., Deotto, L.: Formal methods for the specification and analysis of communication protocols. IEEE Communication Surveys 4(1), 2–20 (2002)
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)
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
Burdett, D.: Internet Open Trading Protocol - IOTP Version 1.0. IETF RFC 2801, Available via (April 2000), http://www.ietf.org/rfc/rfc2801
Burdett, D., Eastlake, D.E., Goncalves, M.: Internet Open Trading Protocol. McGraw-Hill, New York (2000)
Clarke, E.M., Wing, J.M.: Formal methods: state of the art and future directions. ACM Computing Surveys 28(4), 626–643 (1996)
InterPay I-OTP (August 2001), http://www.ietf.org/proceedings/01aug/slides/trade-1/index.html
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)
Jensen, K.: Basic Concepts, Analysis Methods and Practical Use. In: Analysis Methods, 2nd edn. Monographs in Theoretical Computer Science, vol. 2, Springer, Berlin (1997)
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
Mondex, http://www.mondexusa.com
Design/CPN Online, http://www.daimi.au.dk/designCPN
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)
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)
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)
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)
Standard SMart Card Integrated SettLEment System Project SMILE Project (April 1999), http://www.ietf.org/proceedings/99mar/slides/trade-smile-99mar
Visa and MasterCard. SET Secure Electronic Transaction Specification. Vol. 1-3 (May 1997), Available via http://www.setco.org/setspecifications.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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