Formal Analysis of Two Buyer-Seller Watermarking Protocols

In this paper we demonstrate how the formal model constructed in Our previous work [1], 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 [2], an examplar of the Offline Watermarking Authority (OFWA) Model, dean filled ill the framework by Poh and Martin [3]. Second, we model the Shao protocol [4] as, all 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. [5] on the Memon and Wong protocol and we identify a new unbinding attack oil the protocol proposed by Shao.