Analysis of the SET e-commerce protocol using a true concurrency process algebra

ABSTRACT

A formal specification of the purchase phase in the SET protocol (Secure Electronic Transaction), an e-commerce protocol by Visa and MasterCard, is presented. It is modelled by means of a True Concurrency Timed Process Algebra called BTC which takes into account that the (limited amount of) available resources in a system have to be shared by all the processes. We have considered heterogeneous resources and we extend the algebra with the intention of representing the actions which use the shared resources and how many resources of each type the system has at its disposal.

REFERENCES

• 1: Giampaolo Bella , Lawrence C. Paulson , Fabio Massacci, The verification of an industrial payment protocol: the SET purchase phase, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586113]
• 2: G. Bella, F. Massacci, and L. C. Paulson. Verifying the SET registration protocols. In Proceedings of IEEE J. of Selected Areas in Communications, pages 21(1):77--87, 2003.
• 3: Patrice Brémond-Grégoire , Insup Lee, A process algebra of communicating shared resources with dense time and priorities, Theoretical Computer Science, v.189 n.1-2, p.179-219, Dec. 15, 1997 [doi>10.1016/S0304-3975(96)00229-0]
• 4: Mikael Buchholtz, Jacob Andersen, and Hans Henrik Løvengreen. Towards a Process Algebra for Shared Processors. Electronic Notes in Theoretical Computer Science, 52, 2002.
• 5: Gerardo Costa , Colin Stirling, Weak and strong fairness in CCS, Information and Computation, v.73 n.3, p.207-244, June 1987 [doi>10.1016/0890-5401(87)90013-7]
• 6: Fernando Cuartero , David de Frutos-Escrig , Valentín Valero Ruiz, A Sound and Complete Proof System for Probabilistic Processes, Proceedings of the 4th International AMAST Workshop on Real-Time Systems and Concurrent and Distributed Software: Transformation-Based Reactive Systems Development, p.340-352, May 21-23, 1997
• 7: A. O. Freier, P. Karlton, and P. C. Kocher. The SSL protocol v3.0. Internet Draft, 1996.
• 8: A. Giacalone, C.-C. Jou, and S. A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proceedings of Working Conference on Programming Concepts and Methods, IFIP TC 2, Sea of Galilee, Israel, 1990.
• 9: Damas P. Gruska. Process Algebra for Limited Parallelism. In Proc. of Concurrency, Specification and Programming (CS&P'96), pages 61--74, 1996.
• 10: Damas P. Gruska, Bounded Concurrency, Proceedings of the 11th International Symposium on Fundamentals of Computation Theory, p.198-209, September 01-03, 1997
• 11: Holger Hermanns , Ulrich Herzog , Joost-Pieter Katoen, Process algebra for performance evaluation, Theoretical Computer Science, v.274 n.1-2, p.43-87, March 6, 2002 [doi>10.1016/S0304-3975(00)00305-4]
• 12: Jane Hillston, A compositional approach to performance modelling, Cambridge University Press, New York, NY, 1996
• 13: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 14: I. Lee, P. Brémond-Grégoire, and R. Gerber. A process algebraic approach to the specification and analysis of resource-bound real-time systems, 1994.
• 15: Mastercard and VISA. SET Secure Electronic Transaction Specification. http://www.setco.org/set_specifications.html, 1997.
• 16: Faron Moller , Chris Tofts, A temporal calculus of communicating systems, Proceedings on Theories of concurrency : unification and extension: unification and extension, p.401-415, September 1990, Amsterdam, The Netherlands
• 17: Manuel Núñez , David de Frutos-Escrig , Luis Fernando Llana Díaz, Acceptance Trees for Probabilistic Processes, Proceedings of the 6th International Conference on Concurrency Theory, p.249-263, August 21-24, 1995
• 18: G. M. Reed , A. W. Roscoe, A timed model for communicating sequential processes, Theoretical Computer Science, v.58 n.1-3, p.249-261, June 1988 [doi>10.1016/0304-3975(88)90030-8]
• 19: M. C. Ruiz, D. Cazorla, F. Cuartero, J. J. Pardo, and H. Macia. A bounded true concurrency process algebra for performance evaluation. In Proc. of the 1st European Performance Engineering Workshop (EPEW'04), LNCS 3236, pages 143--155, Toledo, Spain, October 2004. Springer.
• 20: M. Carmen Ruiz , Diego Cazorla , Fernando Cuartero , Juan Jose Pardo, A Formal Specification and Performance Evaluation of the Purchase Phase in the SET Protocol, Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, p.239, September 25-29, 2005 [doi>10.1109/SYNASC.2005.4]
• 21: J. J. M. M. Rutten , J. I. Zucker, A semantic approach to fairness, Fundamenta Informaticae, v.16 n.1, p.1-38, Jan. 1992
• 22: D. H. Steves, C. Edmondson-Yurkanan, and M. Gouda. A protocol for secure transactions. In Proceedings of the Second USENIX Workshop on Electronic Commerce., pages 201--212, 1996.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.4 PERFORMANCE OF SYSTEMS

Additional Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.3 Concurrent Programming
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory

Keywords:
SET protocol, formal specification, heterogeneous shared resources, performance evaluation, process algebra