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 http://www.fsel.com/)
The reader is also referred to Roscoe's CSP script(s) of the Needham Schroeder (Lowe) protocol, found at http://web2.comlab.ox.ac.uk/oucl/publications/books/concurrency/, 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|
|Abstract:||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
||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.