Nuovo DRM Paradiso: Designing a Secure, Verified, Fair Exchange DRM Scheme

• Autorzy: Dashti M.T. , Nair S.K. , Jonker H.
• Języki publikacji: EN

Abstrakty

EN

We introduce Nuovo DRM, a digital rights management scheme aimed to provide formal and practical security. The scheme is based on a recent DRM scheme, which we formally specify in the ěCRL process algebraic language. The original scheme stated the following security requirements: effectiveness, secrecy and resistance of content masquerading. We formalise these security requirements as well as strong fairness and formally check the original scheme against these requirements. This verification step uncovered several security weaknesses, which are addressed by Nuovo DRM. In addition to that, Nuovo DRM introduces several procedural practices to enhance the practical security of the scheme. A finite model of Nuovo DRM is subsequently model-checked and shown to satisfy its design requirements, including secrecy, fairness and resistance to content masquerading.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 89, nr 4
• Strony: 393--417
• Opis fizyczny: bibliogr. 35 poz.

Twórcy

autor

Dashti M.T.

autor

Nair S.K.

autor

Jonker H.

• Eindhoven University of Technology, P.O. Box 513, 5600 MB Eindhoven, Netherlands,

Bibliografia

• [1] Abadi, M., Blanchet, B.: Computer-Assisted Verification of a Protocol for Certified Email, SAS '03, 2694, 2003.
• [2] Alpern, B., Schneider, F.: Defining Liveness, Technical Report TR 85-650, Dept. of Computer Science, Cornell University, Ithaca, NY, October 1984.
• [3] Asokan, N.: Fairness in electronic commerce, PhD thesis, Univ.Waterloo, 1998.
• [4] Avoine, G., Gärtner, F., Guerraoui, R., Vukolic, M.: Gracefully Degrading Fair Exchange with Security Modules., EDCC '05, 3463, Springer, 2005.
• [5] Basu, A., Charron-Bost, B., Toueg, S.: Simulating Reliable Links with Unreliable Links in the Presence of Process Crashes, ACM WDAG '96, 1151, Springer, 1996, ISBN 3-540-61769-8.
• [6] Bella, G., Paulson, L. C.: Mechanical Proofs about a Non-repudiation Protocol, TPHOL'01, 2152, Springer, 2001.
• [7] Blom, S., Calamé, J., Lisser, B., Orzan, S., Pang, J., van de Pol, J. C., Torabi Dashti,M.,Wijs, A.: Distributed Analysis with μCRL, TACAS '07, 4424, Springer, 2007.
• [8] Blom, S., Fokkink, W., Groote, J. F., van Langevelde, I., Lisser, B., van de Pol, J. C.: μCRL: A Toolset for Analysing Algebraic Specifications, CAV'01, 2102, Springer, 2001, ISBN 3-540-42345-1.
• [9] Cederquist, J., Torabi Dashti, M.: An Intruder Model for Verifying Termination in Security Protocols, Technical Report TR-CTIT-05-29, University of Twente, Enschede, The Netherlands, 2005.
• [10] Cederquist, J., Torabi Dashti, M.: An Intruder Model for Verifying Liveness in Security Protocols, FMSE '06, ACM Press, 2006.
• [11] Cervesato, I.: Data Access Specification and the Most Powerful Symbolic Attacker in MSR, ISSS '02, 2609, Springer, 2003.
• [12] Clarke, E., Grumberg, O., Peled, D.: Model Checking, MIT Press, 2000.
• [13] Comon, H., Shmatikov, V.: Is it possible to decide whether a cryptographic protocol is secure or not?, J. of Telecomm. and Inform. Tech., 4, 2002, 3-13.
• [14] Dolev, D., Yao, A.: On the security of public key protocols, IEEE Trans. on Information Theory, IT-29(2), 1983, 198-208.
• [15] Evans, N., Schneider, S.: Verifying security protocols with PVS: widening the rank function approach, J. Logic and Algebraic Programming, 64(2), 2005, 253-284.
• [16] Even, S., Yacobi, Y.: Relations amoung public key signature systems, Technical Report 175, Computer Science Department, Technicon, Haifa, Israel, 1980.
• [17] Fernandez, J.-C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP: A Protocol Validation and Verification Toolbox, CAV '98, 1102, Springer, 1996.
• [18] Fischer,M., Lynch, N., Paterson,M.: Impossibility of distributed consensus with one faulty process, J. ACM, 32(2), 1985, 374-382.
• [19] Francez, N.: Fairness, Springer, 1986.
• [20] Groote, J. F., Ponse, A.: The syntax and semantics of μCRL, Algebra of Communicating Processes '94, Workshops in Computing Series, Springer, 1995.
• [21] Gürgens, S., Rudolph, C., Vogt, H.: On the Security of Fair Non-repudiation Protocols, ISC '03, 2851, 2003.
• [22] Halderman, J., Felten, E.: Lessons from the Sony CD DRM Episode, the 15th USENIX Security Symposium, 2006.
• [23] Heather, J., Lowe, G., Schneider, S.: How to Prevent Type Flaw Attacks on Security Protocols, CSFW '00, IEEE CS, 2000.
• [24] Jonker, H. L., Krishnan Nair, S., Torabi Dashti, M.: Nuovo DRM Paradiso, Technical Report SEN-R0602, CWI, Amsterdam, The Netherlands, 2006, http://ftp.cwi.nl/CWIreports/SEN/SEN-R0602.pdf.
• [25] Kähler, D., Küsters, R.: Constraint Solving for Contract-Signing Protocols., CONCUR '05, 3653, Springer, 2005.
• [26] Kremer, S., Markowitch, O., Zhou, J.: An Intensive Survey of Non-repudiation protocols, Computer Communications, 25(17), 2002, 1606-1621.
• [27] Kremer, S., Raskin, J.: A Game-Based Verification of Non-repudiation and Fair Exchange Protocols, CONCUR' 01, 2154, Springer, 2001.
• [28] Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free μ-calculus, Sci. Comput. Program., 46(3), 2003, 255-281, ISSN 0167-6423.
• [29] Meadows, C.: Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends, IEEE J. Selected Areas in Communication, 21(1), 2003, 44-54.
• [30] Nair, S., Popescu, B., Gamage, C., Crispo, B., Tanenbaum, A.: Enabling DRM-preserving digital content redistribution, 7th IEEE Conf. E-Commerce Technology, IEEE CS, 2005.
• [31] Pagnia, H., Vogt, H., Gärtner, F.: Fair Exchange., Comput. J., 46(1), 2003, 55-75.
• [32] Pnueli, A., Xu, J., Zuck, L. D.: Liveness with (0, 1,1)-Counter Abstraction, CAV, 2002.
• [33] van de Pol, J. C., Valero Espada, M.: Modal Abstractions in μCRL, AMAST, 2004.
• [34] Pucella, R., Weissman, V.: A logic for reasoning about digital rights, CSFW '02, IEEE CS, 2002, ISBN 0-7695-1689-0.
• [35] Shmatikov, V., Mitchell, J.: Finite-state analysis of two contract signing protocols, Theor. Comput. Sci., 283(2), 2002, 419-450, ISSN 0304-3975.