{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:05:43Z","timestamp":1742393143518},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540756972"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75698-9_3","type":"book-chapter","created":{"date-parts":[[2007,10,3]],"date-time":"2007-10-03T22:26:03Z","timestamp":1191450363000},"page":"33-48","source":"Crossref","is-referenced-by-count":6,"title":["Nuovo DRM Paradiso: Towards a Verified Fair DRM Scheme"],"prefix":"10.1007","author":[{"given":"M.","family":"Torabi Dashti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Krishnan Nair","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H. L.","family":"Jonker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","first-page":"151","volume-title":"7th IEEE Conf. E-Commerce Technology","author":"S. Nair","year":"2005","unstructured":"Nair, S., Popescu, B., Gamage, C., Crispo, B., Tanenbaum, A.: Enabling DRM-preserving digital content redistribution. In: 7th IEEE Conf. E-Commerce Technology, pp. 151\u2013158. IEEE CS, Los Alamitos (2005)"},{"key":"3_CR2","unstructured":"Halderman, J., Felten, E.: Lessons from the Sony CD DRM episode. In: The 15th USENIX Security Symposium, pp. 77\u201392 (2006)"},{"key":"3_CR3","series-title":"Workshops in Computing Series","doi-asserted-by":"crossref","first-page":"26","DOI":"10.1007\/978-1-4471-2120-6_2","volume-title":"Algebra of Communicating Processes 1994","author":"J.F. Groote","year":"1995","unstructured":"Groote, J.F., Ponse, A.: The syntax and semantics of \u03bcCRL. In: Algebra of Communicating Processes 1994. Workshops in Computing Series, pp. 26\u201362. Springer, Heidelberg (1995)"},{"key":"3_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"250","DOI":"10.1007\/3-540-44585-4_23","volume-title":"Computer Aided Verification","author":"S. Blom","year":"2001","unstructured":"Blom, S., Fokkink, W., Groote, J.F., van Langevelde, I., Lisser, B., van de Pol, J.: \u03bcCRL: A toolset for analysing algebraic specifications. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 250\u2013254. Springer, Heidelberg (2001)"},{"key":"3_CR5","unstructured":"Blom, S., Calame, J., Lisser, B., Orzan, S., Pang, J., van de Pol, J., Torabi Dashti, M., Wijs, A.: Distributed analysis with \u03bcCRL. In: TACAS 2007 (to appear, 2007)"},{"issue":"2","key":"3_CR6","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. on Information Theory\u00a0IT-29(2), 198\u2013208 (1983)","journal-title":"IEEE Trans. on Information Theory"},{"key":"3_CR7","unstructured":"Asokan, N.: Fairness in electronic commerce. PhD thesis, Univ. Waterloo (1998)"},{"key":"3_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1007\/11408901_5","volume-title":"Dependable Computing - EDCC 2005","author":"G. Avoine","year":"2005","unstructured":"Avoine, G., G\u00e4rtner, F., Guerraoui, R., Vukolic, M.: Gracefully degrading fair exchange with security modules. In: Dal Cin, M., Ka\u00e2niche, M., Pataricza, A. (eds.) EDCC 2005. LNCS, vol.\u00a03463, pp. 55\u201371. Springer, Heidelberg (2005)"},{"key":"3_CR9","first-page":"282","volume-title":"CSFW 2002","author":"R. Pucella","year":"2002","unstructured":"Pucella, R., Weissman, V.: A logic for reasoning about digital rights. In: CSFW 2002, pp. 282\u2013294. IEEE CS, Los Alamitos (2002)"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/10958513_15","volume-title":"Information Security","author":"S. G\u00fcrgens","year":"2003","unstructured":"G\u00fcrgens, S., Rudolph, C., Vogt, H.: On the security of fair non-repudiation protocols. In: Boyd, C., Mao, W. (eds.) ISC 2003. LNCS, vol.\u00a02851, pp. 193\u2013207. Springer, Heidelberg (2003)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/3-540-44685-0_37","volume-title":"CONCUR 2001 - Concurrency Theory","author":"S. Kremer","year":"2001","unstructured":"Kremer, S., Raskin, J.: A game-based verification of non-repudiation and fair exchange protocols. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol.\u00a02154, pp. 551\u2013565. Springer, Heidelberg (2001)"},{"issue":"2","key":"3_CR12","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1016\/S0304-3975(01)00141-4","volume":"283","author":"V. Shmatikov","year":"2002","unstructured":"Shmatikov, V., Mitchell, J.: Finite-state analysis of two contract signing protocols. Theor. Comput. Sci.\u00a0283(2), 419\u2013450 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/11539452_20","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"D. K\u00e4hler","year":"2005","unstructured":"K\u00e4hler, D., K\u00fcsters, R.: Constraint solving for contract-signing protocols. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 233\u2013247. Springer, Heidelberg (2005)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-44898-5_17","volume-title":"Static Analysis","author":"M. Abadi","year":"2003","unstructured":"Abadi, M., Blanchet, B.: Computer-assisted verification of a protocol for certified email. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 316\u2013335. Springer, Heidelberg (2003)"},{"key":"3_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/3-540-44755-5_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Bella","year":"2001","unstructured":"Bella, G., Paulson, L.C.: Mechanical proofs about a non-repudiation protocol. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 91\u2013104. Springer, Heidelberg (2001)"},{"issue":"2","key":"3_CR16","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.jlap.2004.09.005","volume":"64","author":"N. Evans","year":"2005","unstructured":"Evans, N., Schneider, S.: Verifying security protocols with PVS: widening the rank function approach. J. Logic and Algebraic Programming\u00a064(2), 253\u2013284 (2005)","journal-title":"J. Logic and Algebraic Programming"},{"key":"3_CR17","unstructured":"Krishnan Nair, S., Torabi Dashti, M.: DRM paradiso (2007), \n                  \n                    http:\/\/www.few.vu.nl\//∼srijith\/paradiso\/andformal.phptherein"},{"issue":"1","key":"3_CR18","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1093\/comjnl\/46.1.55","volume":"46","author":"H. Pagnia","year":"2003","unstructured":"Pagnia, H., Vogt, H., G\u00e4rtner, F.: Fair exchange. Comput. J.\u00a046(1), 55\u201375 (2003)","journal-title":"Comput. J."},{"key":"3_CR19","unstructured":"Alpern, B., Schneider, F.: Defining liveness. Technical Report TR 85-650, Dept. of Computer Science, Cornell University, Ithaca, NY (October 1984)"},{"issue":"2","key":"3_CR20","doi-asserted-by":"publisher","first-page":"374","DOI":"10.1145\/3149.214121","volume":"32","author":"M. Fischer","year":"1985","unstructured":"Fischer, M., Lynch, N., Paterson, M.: Impossibility of distributed consensus with one faulty process. J. ACM\u00a032(2), 374\u2013382 (1985)","journal-title":"J. ACM"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1007\/3-540-61769-8_8","volume-title":"Distributed Algorithms","author":"A. Basu","year":"1996","unstructured":"Basu, A., Charron-Bost, B., Toueg, S.: Simulating reliable links with unreliable links in the presence of process crashes. In: Babao\u011flu, \u00d6., Marzullo, K. (eds.) WDAG 1996. LNCS, vol.\u00a01151, pp. 105\u2013122. Springer, Heidelberg (1996)"},{"key":"3_CR22","unstructured":"Even, S., Yacobi, Y.: Relations amoung public key signature systems. Technical Report 175, Computer Science Department, Technicon, Haifa, Israel (1980)"},{"key":"3_CR23","unstructured":"Jonker, H., Nair, S.K., Dashti, M.T.: Nuovo DRM paradiso. Technical Report SEN-R0602, CWI, Amsterdam, The Netherlands (2006), \n                  \n                    ftp.cwi.nl\/CWIreports\/SEN\/SEN-R0602.pdf"},{"key":"3_CR24","volume-title":"Model Checking","author":"E. Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"issue":"1","key":"3_CR25","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1109\/JSAC.2002.806125","volume":"21","author":"C. Meadows","year":"2003","unstructured":"Meadows, C.: Formal methods for cryptographic protocol analysis: Emerging issues and trends. IEEE J. Selected Areas in Communication\u00a021(1), 44\u201354 (2003)","journal-title":"IEEE J. Selected Areas in Communication"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"437","DOI":"10.1007\/3-540-61474-5_97","volume-title":"Computer Aided Verification","author":"J.C. Fernandez","year":"1996","unstructured":"Fernandez, J.C., Garavel, H., Kerbrat, A., Mateescu, R., Mounier, L., Sighireanu, M.: CADP: A protocol validation and verification toolbox. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 437\u2013440. Springer, Heidelberg (1996)"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"384","DOI":"10.1007\/3-540-36532-X_23","volume-title":"Software Security \u2013 Theories and Systems","author":"I. Cervesato","year":"2003","unstructured":"Cervesato, I.: Data access specification and the most powerful symbolic attacker in MSR. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol.\u00a02609, pp. 384\u2013416. Springer, Heidelberg (2003)"},{"issue":"17","key":"3_CR28","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1016\/S0140-3664(02)00049-X","volume":"25","author":"S. Kremer","year":"2002","unstructured":"Kremer, S., Markowitch, O., Zhou, J.: An intensive survey of non-repudiation protocols. Computer Communications\u00a025(17), 1606\u20131621 (2002)","journal-title":"Computer Communications"},{"key":"3_CR29","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/1180337.1180340","volume-title":"FMSE 2006","author":"J. Cederquist","year":"2006","unstructured":"Cederquist, J., Torabi Dashti, M.: An intruder model for verifying liveness in security protocols. In: FMSE 2006, pp. 23\u201332. ACM Press, New York (2006)"},{"issue":"3","key":"3_CR30","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/S0167-6423(02)00094-1","volume":"46","author":"R. Mateescu","year":"2003","unstructured":"Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free \u03bc-calculus. Sci. Comput. Program.\u00a046(3), 255\u2013281 (2003)","journal-title":"Sci. Comput. Program."},{"key":"3_CR31","first-page":"3","volume":"4","author":"H. Comon","year":"2002","unstructured":"Comon, H., Shmatikov, V.: Is it possible to decide whether a cryptographic protocol is secure or not? J. of Telecomm. and Inform. Tech.\u00a04, 3\u201313 (2002)","journal-title":"J. of Telecomm. and Inform. Tech."},{"key":"3_CR32","first-page":"255","volume-title":"CSFW 2000","author":"J. Heather","year":"2000","unstructured":"Heather, J., Lowe, G., Schneider, S.: How to prevent type flaw attacks on security protocols. In: CSFW 2000, pp. 255\u2013268. IEEE CS, Los Alamitos (2000)"},{"key":"3_CR33","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4886-6","volume-title":"Fairness","author":"N. Francez","year":"1986","unstructured":"Francez, N.: Fairness. Springer, Heidelberg (1986)"}],"container-title":["Lecture Notes in Computer Science","International Symposium on Fundamentals of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75698-9_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:27:39Z","timestamp":1619504859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75698-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540756972"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75698-9_3","relation":{},"subject":[]}}