Enhancing formal specification and verification of e-commerce protocol

  • Authors

    • Hasan Al-Refai Philadelphia University
    • Khaldoun Batiha Philadelphia University
    2017-02-26
    https://doi.org/10.14419/jacst.v6i1.6713
  • SET Protocol, Cryptographic Protocol, SPI and PH-SPI Calculus, Authentication and Privacy.

  • Lots of work have been attempted to enhance the SET protocol performance special attention is on E-payment phase. This paper thoroughly analyzes recent works on payment phase; it has been found that this subject requires considerable enhancements, since there are areas, which require further study such as: E-payment phase in SET protocol.

    E-payment phase is vast and complex phase it has long series of steps. The behavior of environment is assumed by the phase and is restricted to the rules built by their proposed protocol. This paper will follow Ph-Spi calculus for formalizing and analyzing enhanced payment phase of SET protocol by reducing the number of transactions with many additional operators.

    A new agent controller will be formally modeled, which we can rely upon to make automated decisions during interaction with a dynamic protocol environment. So, this agent controller is used to terminate the transaction process in any case of fraud or attack. This paper is conjunction between our previous works of E-payment phase in SET protocol and other works in Ph-Spi calculus in purpose of analyzing and proving the main security properties: authentication and privacy to evaluate the efficiency of the enhanced security of electronic payment phase for SET protocol (E-SET) using Ph-Spi calculus.

  • References

    1. [1] Singh, S, (2009). "Emergence of payment systems in the age of electronic commerce: The state of art," Internet, 2009. AH-ICI 2009. First Asian Himalayas International Conference on, vol., no., pp.1-18, 3-5 Nov. 2009.

      [2] Zhang Xuan, Huang Qinlong and Peng Peng, (2010). "Implementation of a suggested E-commerce model based on SET protocol". Eighth ACIS International Conference on Software Engineering Research, Management and Applications. IEEE, 2010.

      [3] Hasan Al-Refai, Ali Alwaneh, Khaldoun Batiha, Ahmad Jarah. (2014). Enhanced model of Payment Phase for SET Protocol. International Journal of Video&Image Processing and Network Security IJVIPNS-IJENS Vol: 14 No: 0 1.

      [4] A.A.Koponen. (2006). E-COMMERCE, ELECTRONIC PAYMENTS. http://www.cse.tkk.fi/f i/opinnot/T-109.7510/2006/E-commerce.pdf.

      [5] Anssi Mattila. SET & SSL: IS THERE A COMPARISON FOR A GOOD NIGHT SLEEP. International Journal of Enterprise Computing and Business Systems. Volume 2 Issue 2 July 2012.

      [6] Al-Refai (2009) Evaluation Technique in the Spi-Calculus for Cryptographic Protocols. Third International Symposium on Innovation in Information Communication Technology- ISIICT.

      [7] Laudon Kenneth C. and Traver Carol Guercio, (2005). "E-Commerce, Business. Technology". Society. Second edition.

      [8] M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The Spi calculus. Information and Computation, 148(1):1–70, 1999. https://doi.org/10.1006/inco.1998.2740.

      [9] D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198–208, 1983. https://doi.org/10.1109/TIT.1983.1056650.

      [10] G. Bella, F. Massacci, L. C. Paulson, and P. Tramontano. Formal verification of cardholder registration in SET. In Proc. 6th European Symposium on Research in Computer Security (ESORICS), volume 1895 of LNCS, pages 159–174. Springer, 2000. https://doi.org/10.1007/10722599_10.

      [11] C. Meadows and P. Syverson. A formal specification of requirements for payment transactions in the SET protocol. In Proc. 2nd Financial Cryptography Conference (FC), volume 1465 of LNCS, pages 122–140. Springer, 1998. https://doi.org/10.1007/BFb0055477.

      [12] M. Abadi and A. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5(4):267–303, 1998. https://doi.org/10.1007/bfb0053560.

      [13] R. Milner Communicating and Mobile System: the pi-Calculus. Cambridge University Press, 1999.

      [14] Hasan Al-Refai, Khaldoun Batiha, Ali Alwaneh, Saleh Bani Hani. (2014). Improved SPI Calculus for Reasoning on Cryptographic Protocols. International Journal of Video&Image Processing and Network Security IJVIPNS-IJENS Vol:14 No:01

      [15] M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The Spi Calculus. Information and Computation, 148(1):1–70, January 1999. Full version available as SRC Research Report 149, January 1998.

      [16] M. Abadi and A. Gordon. Reasoning about cryptographic protocols in the Spi Calculus. In A. Mazurkiewicz and J. Winkowski, editors, Proceedings of the 8th International Conference on Concurrency Theory (CONCUR), volume 1243 of Lecture Notes in Computer Science, pages 59–73, Warsaw, Poland, July 1997. Springer. https://doi.org/10.1007/3-540-63141-0_5.

      [17] Martin Abadi and Cedric Fournet. “Mobile values, new names, and secure communicationâ€. POPL 2001.

      [18] Horea and Florian Boian. OrosSpi calculus analysis of Otway-Rees protocol. International Journal of Computers, Communications & Control (IJCCC) 3:427-432 • January 2008.

      [19] Pedro Adao. "Electronic Money within My-Calculus". Applied Mathematics and Computation Diploma Thesis. July 2002.

      [20] Laszlo Aszalos and Andrea Huszti. "Applying Spi-Calculus for PayWord". Eighth International Conference on Applied Informatics. 2010.

      [21] Giampaolo Bella, Fabio Massacci and Lawrence C Paulson. Verifying the SET Purchase Protocols. Kluwer Academic Publishers. Printed in the Netherlands. 2005.s

      [22] Zihao Shen; Hui Wang, (2010). "An improved SET protocol payment system," Computer and Communication Technologies in Agriculture Engineering (CCTAE), 2010 International Conference On , vol.1, no., pp.400-403, 12-13 June 2010.

      [23] Li Yabo, (2008). "The Design of the Secure Electronic Payment System Based on the SET Protocol," ICCSIT, pp.29-33, 2008 International Conference on Computer Science and Information Technology. https://doi.org/10.1109/ICCSIT.2008.175.

      [24] Fei Xu, Zhang Ai Ming and Liang Wan, (2010). "Formalizing and Checking SET Protocol Based on TLA." IEEE, 2010.

      [25] Hassan M. Elkamchouchi 1, Eman F. Abu Elkhair2 and Yasmine Abouelseoud3. AN IMPROVEMENT TO THE SET PROTOCOL BASED ON SIGNCRYPTION.. International Journal on Cryptography and Information Security (IJCIS), Vol.3, No. 2, June 2013.

      [26] Y. LI AND Y. WANG, "SECURE ELECTRONIC TRANSACTION (SET PROTOCOL)", [ONLINE] AVAILABLE AT HTTP://WWW .PEOPLE.DSV. SU.SE/~MATEI/COURSES/IK2001_SJE/LI-WANG_SET.PDF 2012.

      [27] Boping Zhang, and Shiyu Shang, (2009). An Improved SET Protocol. Proceedings of the 2009 International Symposium on Information Processing (ISIP’09) Huangshan, P. R. China, August 21-23, 2009, pp. 267-272.

      [28] Xu Yong and Liu Jindi, (2010). "Electronic Payment System Design Based on SET and TTP," ICEE, pp.275-278, 2010 International Conference on E-Business and E-Government, 2010. https://doi.org/10.1109/ICEE.2010.77.

  • Downloads

  • How to Cite

    Al-Refai, H., & Batiha, K. (2017). Enhancing formal specification and verification of e-commerce protocol. Journal of Advanced Computer Science & Technology, 6(1), 13-19. https://doi.org/10.14419/jacst.v6i1.6713