A Formal Approach to the Analysis of Protocols Protecting IPR
- When?
- Wednesday 16 September 2009, 14:00 to 15:00
- Where?
- 39 BB 02
- Open to:
- Students, Staff
- Speaker:
- 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 copyright owners to track piracy to a single transaction; thus watermarking is a technique used for transaction tracking. However, for the solution to be deemed fair, it is imperative that both consumers and content creators are satisfied by such a technological solution. To this end, Buyer-Seller Watermarking (BSW) protocols have been developed to be used in conjunction with digital watermarking schemes.
The work recorded in this report demonstrates our success in finding attacks on BSW protocols using the process algebra Communicating Sequential Processes (CSP) and the model checker Failures-Divergence-Refinement (FDR). Following a review of the literature regarding security protocol analysis, we construct a formal definition of fair transaction tracking and assess whether three published BSW protocols satisfy this property.