research-article

Modelling watermark communication protocols using the CASPER modelling language

Authors:

Jana DittmannAuthors Info & Claims

MM&Sec '10: Proceedings of the 12th ACM workshop on Multimedia and security

Pages 107 - 116

https://doi.org/10.1145/1854229.1854252

Published: 09 September 2010 Publication History

Get Access

Abstract

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.

References

[1]

S. Katzenbeisser: Computational Security Models for Digital Watermarks. In Workshop on Image Analysis for Multimedia Interactive Services (WIAMIS 2005), 2005.

Google Scholar

[2]

G. Lowe: CASPER: A Compiler for the Analysis of Security Protocols. Journal of Computer Security, Society Press, 1998.

Digital Library

Google Scholar

[3]

A. W. Roscoe: Model-checking CSP. In A classical mind: essays in honour of C. A. R. Hoare, Prentice Hall International (UK) Ltd., 1994.

Digital Library

Google Scholar

[4]

FDR user manual. Formal Systems (Europe) Ltd. http://www.fsel.com/documentation/fdr2/html/

Google Scholar

[5]

J. Dittmann, S. Katzenbeisser, C. Schallhart, H. Veith: Ensuring Media Integrity on Third-Party Infrastructures. In 20th IFIP International Information Security Conference(SEC2005), Springer, 2005.

Google Scholar

[6]

A. Lang: Audio Watermarking Benchmarking -- A Profile Based Approach. PhD Thesis. Otto-von-Guericke-University Magdeburg, Germany, Dept. of Computer Science, ISBN: 978--3--940961--22--8, 2007.

Google Scholar

[7]

T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein: Introduction to Algorithms. 2nd ed. MIT Press and McGraw-Hill, ISBN 0--262-03293--7. Section 22.3: Depth-first search, pp. 540--549, 2001.

Digital Library

Google Scholar

[8]

G. Lowe, P. Broadfoot, M. L. Hui: CASPER - A Compiler for the Analysis of Security Protocols. User Manual and Tutorial, Version 1.5, Oxford University Computing Lab, December, 2001.

Google Scholar

[9]

P. Ryan, S. Schneider, M. H. Goldsmith: Modelling and Analysis of Security Protocols. Addison-Wesley Professional, ISBN-13: 978-0201674712, 2000.

Digital Library

Google Scholar

[10]

C. A. R. Hoare: Communicating Sequential Processes. Prentice Hall International, 2004.

Google Scholar

Cited By

View all

Woo-Sik B(2019)Formal Verification of an RFID Authentication Protocol Based on Hash Function and Secret CodeWireless Personal Communications: An International Journal10.1007/s11277-014-1745-879:4(2595-2609)Online publication date: 3-Jan-2019
https://dl.acm.org/doi/10.1007/s11277-014-1745-8
Yong ZAixin ZSongnian L(2013)Group fingerprinting communication protocols for digital wholesale and retail in E-commerce2013 Second International Conference on Informatics & Applications (ICIA)10.1109/ICoIA.2013.6650245(143-146)Online publication date: Sep-2013
https://doi.org/10.1109/ICoIA.2013.6650245
Kraetzer CMerkel RAltschaffel RClausing EDittmann JHeitzenrater CCraver SDittmann J(2011)Semi-automated communication protocol security verification for watermarking - pros and cons illustrated on a complex application scenarioProceedings of the thirteenth ACM multimedia workshop on Multimedia and security10.1145/2037252.2037270(93-102)Online publication date: 29-Sep-2011
https://dl.acm.org/doi/10.1145/2037252.2037270
Show More Cited By

Index Terms

Modelling watermark communication protocols using the CASPER modelling language

Recommendations

Finite-state analysis of two contract signing protocols

Optimistic contract signing protocols allow two parties to commit to a previously agreed upon contract, relying on a third party to abort or confirm the contract if needed. These protocols are relatively subtle, since there may be interactions between ...
Provably secure CL-KEM-based password-authenticated key exchange protocol

Traditional password-based authentication protocols are vulnerable to various password-related attacks, while public key cryptography PKC is expensive to manage certificates. Moreover, the traditional identity-based cryptography suffers to key escrow. ...
Buyer-seller watermarking protocols with off-line trusted third parties

In a buyer-seller watermarking protocol, buyers and sellers protect the ownerships or copyrights of their digital contents through the watermarks embedded in them. However, some known attacks and problems are still threatening the security of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

MM&Sec '10: Proceedings of the 12th ACM workshop on Multimedia and security

September 2010

264 pages

ISBN:9781450302869

DOI:10.1145/1854229

General Chair:
Patrizio Campisi
Università degli Studi Roma TRE, Rome, Italy
,
Program Chairs:
Jana Dittmann
Otto-von-Guericke University Magdeburg, Germany
,
Scott Craver
SUNY Binghamton, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

MM&Sec '10

Sponsor:

SIGMM

MM&Sec '10: Multimedia and Security Workshop

September 9 - 10, 2010

Roma, Italy

Acceptance Rates

Overall Acceptance Rate 128 of 318 submissions, 40%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
135
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Woo-Sik B(2019)Formal Verification of an RFID Authentication Protocol Based on Hash Function and Secret CodeWireless Personal Communications: An International Journal10.1007/s11277-014-1745-879:4(2595-2609)Online publication date: 3-Jan-2019
https://dl.acm.org/doi/10.1007/s11277-014-1745-8
Yong ZAixin ZSongnian L(2013)Group fingerprinting communication protocols for digital wholesale and retail in E-commerce2013 Second International Conference on Informatics & Applications (ICIA)10.1109/ICoIA.2013.6650245(143-146)Online publication date: Sep-2013
https://doi.org/10.1109/ICoIA.2013.6650245
Kraetzer CMerkel RAltschaffel RClausing EDittmann JHeitzenrater CCraver SDittmann J(2011)Semi-automated communication protocol security verification for watermarking - pros and cons illustrated on a complex application scenarioProceedings of the thirteenth ACM multimedia workshop on Multimedia and security10.1145/2037252.2037270(93-102)Online publication date: 29-Sep-2011
https://dl.acm.org/doi/10.1145/2037252.2037270
Merkel RKraetzer CAltschaffel RClausing ESchott MDittmann J(2011)Fingerprint forensics application protocolProceedings of the 10th international conference on Digital-Forensics and Watermarking10.1007/978-3-642-32205-1_26(321-335)Online publication date: 23-Oct-2011
https://dl.acm.org/doi/10.1007/978-3-642-32205-1_26

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Finite-state analysis of two contract signing protocols

Provably secure CL-KEM-based password-authenticated key exchange protocol

Buyer-seller watermarking protocols with off-line trusted third parties