Watermarking gets formal at workshop
Friday 20 June 2008
David Williams, a PhD student in the Department, and colleagues have a paper on the formal analysis of a digital watermarking technique accepted for presentation at the 10th ACM Workshop on Multimedia and Security in Oxford in September.
Williams, D.M.*, Treharne, H., Ho, A.T.S. & Culnane, C. (2008). Using a Formal Analysis Technique to Identify an Unbinding Attack on a Buyer-Seller Watermarking Protocol
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.
*The author's work is sponsored by an EPSRC Thales CASE Award.