Modelling Watermark Communication Protocols using the CASPER Modelling Language

摘要

In cryptography it is common to evaluate the security of cryptographic primitives and protocols in a computational model, with an attacker trying to break the primitive or protocol in question. To do so formalisation languages like CASPER or CSP (Communication Sequential Processes) and model checkers like FDR (Failures-Divergences Refinement) are used for automatic or semi-automatic machine-based security verification. Here we transfer the idea of machine-based verification of the security of communication protocols from cryptography to the domain of digital watermarking based media security protocols. To allow for such a mainly automatic verification approach, We introduce and illustrate in this paper a six step procedure for the modelling and verification of watermark communication protocols based on application scenario descriptions. The six steps are: First, a modelling of the used communication network and application scenario (as a task) in XML-structures, second, a path search comparing the network and the task and identifying possible watermarking channels, third, a path selection selecting one watermarking channel from the identified alternatives for the protocol realisation, fourth, an automatic CASPER protocol generation from the selected alternative followed by manual adjustments (if necessary), fifth, the CASPER compilation into CSP and sixth, the protocol security (confidentiality, integrity and authenticity) verification via the FDR model checker.