The Modelling and Analysis of Buyer-Seller Watermarking Protocols
- When?
- Wednesday 29 June 2011, 10:30 to 11:30
- Where?
- 39BB02
- Open to:
- Staff, Students
- Speaker:
- Mr David Williams
The primary benefit of digital content, the ease with which it can be duplicated and disseminated, is also the primary concern when endeavouring to protect the rights of those creating the content. Copyright owners wish to deter illicit file sharing of copyrighted material, detect it when it occurs and even trace the original perpetrator. Embedding a unique identifying watermark into licensed multimedia content enables those selling digital content to trace illicit acts of file sharing to a single transaction with a single a buyer. However, evidence of such illicit activity must be gathered if and only if the buyer truly shared the content for a seller to prove such behaviour to an arbitrator. For this purpose, Buyer-Seller Watermarking (BSW) protocols have been developed to be used in conjunction with digital watermarking schemes.
The work recorded in this thesis increases the rigour with which BSW protocols are analysed against their requirements. This thesis demonstrates the success of the formal approach we have developed in finding attacks on BSW protocols using the process algebra, Communicating Sequential Processes (CSP), and the model checker, Failures-Divergence-Refinement (FDR). In particular, we construct a formal definition of the requirements of BSW protocols, against which we evaluate five published protocols. We use FDR to automatically generate traces indicative of protocol failures verifying three previously known attacks on BSW protocols and identifying seven otherwise unreported flaws. We describe how our approach can be extended to analyse BSW protocols under alternative assumptions, in order to demonstrate how our approach may endure changes to the properties BSW protocols aim to provide or the environment in which they are to be deployed. Finally, we identify a flaw within Memon and Wong's example construction of their BSW protocol by scrutinising the properties inherent in such a construction, which is based upon the Cox et al.'s secure spread-spectrum watermarking scheme.