University of Surrey Logo

Formal Methods and Security Group

homepage of David M. Williams

Formal Analysis of Buyer-Seller Watermarking Protocols

David M Williams' research within the Department of Computing is conducted in collaboration with Thales Research and Technology. The main theme of the proposed research focuses upon the theoretical modeling, methodology and applications of formal methods on the security verification and validation of digital watermarking systems for multimedia content.

This page provides supporting material for the papers accepted for inclusion within conference proceedings.

The CSP scripts can be used, without modification, in conjunction with various tool support in order to animate, explore and analyse the protocols modelled within them (Probe and FDR
by Formal Systems (Europe) Ltd. can be found at

The reader is also referred to Roscoe's CSP script(s) of the Needham Schroeder (Lowe) protocol, found at, which formed the basis of our work.

Using a Formal Analysis Technique to Identify an Unbinding Attack on a Buyer-Seller Watermarking Protocol pdf


David M. Williams, Helen Treharne, Anthony T.S. Ho and Chris Culnane


MM&Sec: Proceedings of the 10th ACM workshop on Multimedia and Security







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




Formal Analysis of Two Buyer Seller Watermarking Protocols


David M. Williams, Helen Treharne, Anthony T.S. Ho and Adrian Waller


To be included in the proceedings of the 7th International Workshop on Digital Watermarking


In this paper we demonstrate how the formal model constructed in our previous work can be modified in order to analyse additional Buyer-Seller Watermarking Protocols, identifying which specific sections of the CSP scripts remain identical and which require modification. First, we model the protocol proposed by Memon and Wong, an examplar of the Offline Watermarking Authority (OFWA) Model, defined in the framework by Poh and Martin. Second, we model the Shao protocol as an example of a protocol fitting the Online Watermarking Authority (ONWA) Model. Our analysis of the protocols reaffirms the unbinding attack described by Lei et al. on the Memon and Wong protocol and we identify a new unbinding attack on the protocol proposed by Shao.

memon_wong.csp; shao.csp