A Formal Analysis of Buyer-Seller Watermarking Protocols
- When?
- Monday 25 October 2010, 13:30 to 14:30
- Where?
- 39BB02
- Open to:
- Staff, Students
- Speaker:
- Mr David Williams
Copyright owners are faced with the task of limiting illicit file sharing of multimedia content. With this aim, Buyer-Seller Watermarking protocols are proposed to act as a suitable deterrent to file sharing by providing the copyright owner with adequate evidence of illegal distribution if and only if such illicit behaviour has occurred. A recent survey of BSW protocols concluded that only heuristic approaches to the security analysis of such protocols had been adopted in the literature and that formal analysis of the security of such schemes is a research direction worth pursuing.
In this presentation David will demonstrate how we may use Linear Temporal Logic (LTL) to provide the first precise definition of the {\em customers' rights} and present a general approach to the formal modelling of Buyer-Seller watermarking protocols using the process algebra CSP. Using CSP and FDR we verify published flaws in Buyer-Seller Watermarking Protocols and also identify previously unknown attacks.