Abstract
Recently, the technique of semi-automated protocol verification using model-checkers was transferred from cryptography to the domain of watermark-based communication protocols. This technique offers cost-effective security verification of such watermark-based protocols and an increased flexibility in comparison to traditionally applied, manual mathematical proofs. In this paper, we want to evaluate the feasibility of this approach, using the modeling language CASPER and the model-checker FDR. We extract the prospects and limitations of the approach by modeling and verifying a practical application scenario for forensic investigations using high-resolution biometric fingerprint data. We evaluate the security aspects, which can be verified by the scheme, as well as the syntactical limitations, complexity limitations and the methodological limitations and indentify necessary improvements for a practical usage of such scheme.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Pimentel, J.C.L., Monroy, R.: Formal Support to Security Protocol Devel-opment: A Survey. Computación y Sistemas 12(1), 89–108 (2008) ISSN 1405-5546
Kraetzer, C., Merkel, R., Altschaffel, R., Clausing, E., Schott, M., Dittmann, J.: Modelling Watermark Communication Protocols using the CASPER Modelling Language. In: Proc. ACM Multimedia and Security Workshop 2010 (MMSec 2010), Rome, Italy, pp. S.67–S.72. ACM Press, New York (2010) ISBN 978-1-450-30286-9
Lowe, G.: CASPER: A Compiler for the Analysis of Security Protocols. Journal of Computer Security (1998)
FDR user manual. Formal Systems (Europe) Ltd., http://www.fsel.com/documen-tation/fdr2/html/ (last accessed August 30, 2011)
Lowe, G., Broadfoot, P., Dilloway, C., Hui, M.L.: CASPER - A Compiler for the Analysis of Security Protocols. User Manual and Tutorial, Version 1.12, Oxford University Computing Lab (2009)
Roscoe, A.W.: Model-checking CSP. In: A Classical Mind: Essays in Honour of C. A. R. Hoare. Prentice Hall International (UK) Ltd. (1994)
Viganò, L.: Automated Security Protocol Analysis with the AVISPA Tool. In: Proc. XXI Mathematical Foundations of Programming Semantics, MFPS 2005 (2005)
Reactive Objects Language, http://ece.ut.ac.ir/FML/rebeca.htm (last accessed August 30, 2011)
Song, D.X.: Athena: a new efficient automatic checker for security protocol analysis. In: Proceedings of the Twelfth IEEE Computer Security Foundations Workshop, pp. 192–202. IEEE Computer Society Press (1999)
Fries Research Technology, http://www.frt-gmbh.com/en/ (last accessed August 30, 2011)
Newman, R.: Computer forensics: evidence, collection, and management. Auerbach (2007)
Sheppard, N.P., Naini, R.S., Ogunbona, P.: On multiple watermarking. In: Proc. ACM Multimedia and Security Workshop 2001 Ottawa, Ontario, Canada, October 5, pp. 3–6. ACM (2001)
Dittmann, J., Katzenbeisser, S., Schallhart, C., Veith, H.: Provably secure authentication of digital media through invertible watermarks. Cryptology ePrint Archive, Report 2004/293 (2004), http://eprint.iacr.org/
Coltuc, D., Chassery, J.M.: Very fast watermarking by reversible contrast mapping. IEEE Signal Process. Lett. 14(4), 255–258 (2007)
Hui, M.L., Lowe, G.: Safe simplifying transformations for security protocols. In: 12th Computer Security Foundations Workshop Proceedings, pp. 32–43. IEEE Computer Society Press (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Merkel, R., Kraetzer, C., Altschaffel, R., Clausing, E., Schott, M., Dittmann, J. (2012). Fingerprint Forensics Application Protocol: Semi-automated Modeling and Verification of Watermark-Based Communication Using CASPER and FDR. In: Shi, Y.Q., Kim, HJ., Perez-Gonzalez, F. (eds) Digital Forensics and Watermarking. IWDW 2011. Lecture Notes in Computer Science, vol 7128. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32205-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-642-32205-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32204-4
Online ISBN: 978-3-642-32205-1
eBook Packages: Computer ScienceComputer Science (R0)