Using a formal analysis technique to identify an unbinding attack on a buyer-seller watermarking protocol

ABSTRACT

In this paper we provide a novel approach to the analysis of buyer-seller watermarking protocols by tailoring an existing formal technique that has not previously been used in this context. We accurately represent a buyer-seller watermarking protocol as proposed by Ibrahim et al. [6] by constructing a model using the process algebra CSP. By describing our model in this manner and utilising the tool support associated with CSP we are able to conduct a thorough analysis of all the possible behaviour in the protocol. Through formal analysis we have discovered an unbinding attack on the protocol. In this paper we also highlight other weaknesses that exist in the protocol and propose verifiable solutions to correct these weaknesses.

REFERENCES

• 1: C.-C. Chang and C.-. Chung. An enhanced buyer seller watermarking protocol. In International Conference on Communication Technology Proceedings, pages 1779--1783, 2003.
• 2: Ingemar Cox , Matthew L. Miller , Jeffery A. Bloom, Digital watermarking, Morgan Kaufmann Publishers Inc., San Francisco, CA, 2001
• 3: S. Craver, N. Memon, B. L. Yeo, and M. Yeung. Resolving rightful ownerships with invisible watermarking techniques: limitations, attacks, and implications. IEEE Journal on Selected Areas in Communications, 16(4):573--586, 1998.
• 4: D. Dolev and A. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983.
• 5: C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
• 6: Ibrahim M. Ibrahim , Sherif Hazem Nour El-Din , Abdel Fatah A. Hegazy, An Effective and Secure Buyer-Seller Watermarking Protocol, Proceedings of the Third International Symposium on Information Assurance and Security, p.21-28, August 29-31, 2007 [doi>10.1109/IAS.2007.17]
• 7: C.-L. Lei, P.-L. Yu, P.-L. Tsai, and M.-H. Chan. An efficient and anonymous buyer-seller watermarking protocol. IEEE Transactions on Image Processing, 13(12):1618--1626, 2004.
• 8: Gavin Lowe, Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, p.147-166, March 27-29, 1996
• 9: N. Memon and P. W. Wong. A buyer seller watermarking protocol. IEEE Transactions on Image Processing, 10(4):643--649, 2001.
• 10: L. Qiao and K. Nahrstedt. Watermarking schemes and protocols for protecting rightful ownership and customers' rights. Journal of Visual Communication and Image Representation, 9(3):194--210, 1998.
• 11: A. W. Roscoe , C. A. R. Hoare , Richard Bird, The Theory and Practice of Concurrency, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 12: P. Ryan , S. Schneider, The modelling and analysis of security protocols: the csp approach, Addison-Wesley Professional, 2000
• 13: F. Systems. FDR 2.82. Formal Systems Ltd., 2005.
• 14: J. Zhang, W. Kou, and K. Fan. Secure buyer-seller watermarking protocol. IEE Proceedings Information Security, 153(1):15--18, 2006.

INDEX TERMS

Primary Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING

Additional Classification:
  E. Data
  E.m MISCELLANEOUS

General Terms:
Security, Verification

Keywords:
buyer-seller watermarking protocol, csp, customer's rights, formal analysis, formal model, unbinding