{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T02:54:48Z","timestamp":1725504888321},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540786627"},{"type":"electronic","value":"9783540786634"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78663-4_21","type":"book-chapter","created":{"date-parts":[[2008,3,8]],"date-time":"2008-03-08T06:00:01Z","timestamp":1204956001000},"page":"312-329","source":"Crossref","is-referenced-by-count":10,"title":["Formal Proofs of Cryptographic Security of Diffie-Hellman-Based Protocols"],"prefix":"10.1007","author":[{"given":"Arnab","family":"Roy","sequence":"first","affiliation":[]},{"given":"Anupam","family":"Datta","sequence":"additional","affiliation":[]},{"given":"John C.","family":"Mitchell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"2","key":"21_CR1","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s00145-001-0014-7","volume":"15","author":"M. Abadi","year":"2002","unstructured":"Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). Journal of Cryptology\u00a015(2), 103\u2013127 (2002)","journal-title":"Journal of Cryptology"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"Ad\u00e3o, P., Bana, G., Scedrov, A.: Computational and information-theoretic soundness and completeness of formal encryption. In: Proc. of the 18th IEEE Computer Security Foudnations Workshop, pp. 170\u2013184 (2005)","DOI":"10.1109\/CSFW.2005.13"},{"issue":"4","key":"21_CR3","first-page":"1","volume":"7","author":"W. Aiello","year":"2004","unstructured":"Aiello, W., Bellovin, S.M., Blaze, M., Canetti, R., Ioannidis, J., Keromytis, A.D., Reingold, O.: Just Fast Keying: Key agreement in a hostile internet. ACM Trans. Inf. Syst. Security\u00a07(4), 1\u201330 (2004)","journal-title":"ACM Trans. Inf. Syst. Security"},{"key":"21_CR4","doi-asserted-by":"crossref","unstructured":"Backes, M., Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Cryptographically sound security proofs for basic and public-key Kerberos. In: Proceedings of 11th European Symposium on Research in Computer Security (to appear, 2006)","DOI":"10.1007\/11863908_23"},{"key":"21_CR5","volume-title":"Proc. of the 10th European Symposium on Research in Computer Security","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B.: Limits of the cryptographic realization of XOR. In: Proc. of the 10th European Symposium on Research in Computer Security, Springer, Heidelberg (2005)"},{"key":"21_CR6","first-page":"171","volume-title":"Proc. IEEE Symposium on Security and Privacy","author":"M. Backes","year":"2005","unstructured":"Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. In: Proc. IEEE Symposium on Security and Privacy, pp. 171\u2013182. IEEE Computer Society Press, Los Alamitos (2005)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: A universally composable cryptographic library. Cryptology ePrint Archive, Report 2003\/015 (2003)","DOI":"10.1145\/948138.948140"},{"key":"21_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/11863908_25","volume-title":"Computer Security \u2013 ESORICS 2006","author":"M. Backes","year":"2006","unstructured":"Backes, M., Pfitzmann, B., Waidner, M.: Limits of the reactive simulatability\/UC of Dolev-Yao models with hashes. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 404\u2013423. Springer, Heidelberg (2006)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/BFb0055875","volume-title":"Computer Security \u2013 ESORICS 98","author":"G. Bella","year":"1998","unstructured":"Bella, G., Paulson, L.C.: Kerberos version IV: Inductive analysis of the secrecy goals. In: Quisquater, J.-J., Deswarte, Y., Meadows, C., Gollmann, D. (eds.) ESORICS 1998. LNCS, vol.\u00a01485, pp. 361\u2013375. Springer, Heidelberg (1998)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1007\/3-540-45539-6_18","volume-title":"Advances in Cryptology - EUROCRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Boldyreva, A., Micali, S.: Public-key encryption in a multi-user setting: Security proofs and improvements. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol.\u00a01807, pp. 259\u2013274. Springer, Heidelberg (2000)"},{"key":"21_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/3-540-44448-3_41","volume-title":"Advances in Cryptology - ASIACRYPT 2000","author":"M. Bellare","year":"2000","unstructured":"Bellare, M., Namprempre, C.: Authenticated encryption: Relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol.\u00a01976, pp. 531\u2013545. Springer, Heidelberg (2000)"},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: A paradigm for designing efficient protocols. In: ACM Conference on Computer and Communications Security, pp. 62\u201373 (1993)","DOI":"10.1145\/168588.168596"},{"key":"21_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/3-540-48329-2_21","volume-title":"Advances in Cryptology - CRYPTO \u201993","author":"M. Bellare","year":"1994","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol.\u00a0773, pp. 232\u2013249. Springer, Heidelberg (1994)"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"Boldyreva, A., Kumar, V.: Provable-security analysis of authenticated encryption in Kerberos. In: Proc.\u00a0IEEE Security and Privacy (2007)","DOI":"10.1109\/SP.2007.19"},{"key":"21_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74143-5_27","volume-title":"Advances in Cryptology - CRYPTO 2007","author":"E. Bresson","year":"2007","unstructured":"Bresson, E., Lakhnech, Y., Mazare, L., Warinschi, B.: A Generalization of DDH with Applications to Protocol Analysis and Computational Soundness. In: Menezes, A. (ed.) CRYPTO 2007. LNCS, vol.\u00a04622, Springer, Heidelberg (2007)"},{"key":"21_CR16","doi-asserted-by":"crossref","unstructured":"Butler, F., Cervesato, I., Jaggard, A.D., Scedrov, A.: Verifying confidentiality and authentication in Kerberos. In: ISSS, vol. 5, pp. 1\u201324 (2003)","DOI":"10.1007\/978-3-540-37621-7_1"},{"key":"21_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-44647-8_2","volume-title":"Advances in Cryptology - CRYPTO 2001","author":"R. Canetti","year":"2001","unstructured":"Canetti, R., Fischlin, M.: Universally composable commitments. In: Kilian, J. (ed.) CRYPTO 2001. LNCS, vol.\u00a02139, pp. 19\u201340. Springer, Heidelberg (2001)"},{"key":"21_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/11681878_20","volume-title":"Theory of Cryptography","author":"R. Canetti","year":"2006","unstructured":"Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols. In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol.\u00a03876, pp. 380\u2013403. Springer, Heidelberg (2006)"},{"key":"21_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-540-89439-1","volume-title":"ASIAN 2006","author":"I. Cervesato","year":"2008","unstructured":"Cervesato, I., Jaggard, A., Scedrov, A., Tsay, J.-K., Walstad, C.: Breaking and fixing public-key Kerberos. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 167\u2013181. Springer, Heidelberg (2008)"},{"key":"21_CR20","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: CSFW, pp. 48\u201361 (2005)","DOI":"10.1109\/CSFW.2005.7"},{"key":"21_CR21","unstructured":"Chevassut, O., Fouque, P.-A., Gaudry, P., Pointcheval, D.: Key derivation and randomness extraction. Cryptology ePrint Archive, Report 2005\/061 (2005), http:\/\/eprint.iacr.org\/"},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1007\/978-3-540-31987-0_12","volume-title":"Programming Languages and Systems","author":"V. Cortier","year":"2005","unstructured":"Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 157\u2013171. Springer, Heidelberg (2005)"},{"key":"21_CR23","doi-asserted-by":"crossref","unstructured":"Datta, A., Derek, A., Mitchell, J., Ramanathan, A., Scedrov, A.: Games and the impossibility of realizable ideal functionality. In: TCC, pp. 360\u2013379 (2006)","DOI":"10.1007\/11681878_19"},{"key":"21_CR24","doi-asserted-by":"crossref","first-page":"423","DOI":"10.3233\/JCS-2005-13304","volume":"13","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Pavlovic, D.: A derivation system and compositional logic for security protocols. Journal of Computer Security\u00a013, 423\u2013482 (2005)","journal-title":"Journal of Computer Security"},{"key":"21_CR25","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.entcs.2007.02.012","volume":"172","author":"A. Datta","year":"2007","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Roy, A.: Protocol Composition Logic (PCL). Electronic Notes in Theoretical Computer Science\u00a0172, 311\u2013358 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"21_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/11523468_2","volume-title":"Automata, Languages and Programming","author":"A. Datta","year":"2005","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Shmatikov, V., Turuani, M.: Probabilistic polynomial-time semantics for a protocol security logic. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"21_CR27","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1109\/CSFW.2006.9","volume-title":"Proceedings of 19th IEEE Computer Security Foundations Workshop","author":"A. Datta","year":"2006","unstructured":"Datta, A., Derek, A., Mitchell, J.C., Warinschi, B.: Computationally sound compositional logic for key exchange protocols. In: Proceedings of 19th IEEE Computer Security Foundations Workshop, pp. 321\u2013334. IEEE Computer Society Press, Los Alamitos (2006)"},{"issue":"6","key":"21_CR28","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"IT-22","author":"W. Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory\u00a0IT-22(6), 644\u2013654 (1976)","journal-title":"IEEE Transactions on Information Theory"},{"key":"21_CR29","doi-asserted-by":"crossref","unstructured":"He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A modular correctness proof of IEEE 802.11i and TLS. In: ACM Conference on Computer and Communications Security, pp. 2\u201315 (2005)","DOI":"10.1145\/1102120.1102124"},{"key":"21_CR30","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1109\/CSFW.2003.1212716","volume-title":"Proceedings of 16th IEEE Computer Security Foundations Workshop","author":"J. Herzog","year":"2003","unstructured":"Herzog, J.: The Diffie-Hellman key-agreement scheme in the strand-space model. In: Proceedings of 16th IEEE Computer Security Foundations Workshop, pp. 234\u2013247. IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"21_CR31","unstructured":"Herzog, J.: Computational Soundness for Standard Assumptions of Formal Cryptography. PhD thesis, MIT (2004)"},{"key":"21_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"172","DOI":"10.1007\/978-3-540-31987-0_13","volume-title":"Programming Languages and Systems","author":"R. Janvier","year":"2005","unstructured":"Janvier, R., Mazare, L., Lakhnech, Y.: Completing the picture: Soundness of formal encryption in the presence of active adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 172\u2013185. Springer, Heidelberg (2005)"},{"key":"21_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-44706-7_20","volume-title":"Fast Software Encryption","author":"J. Katz","year":"2001","unstructured":"Katz, J., Yung, M.: Unforgeable encryption and chosen ciphertext secure modes of operation. In: Schneier, B. (ed.) FSE 2000. LNCS, vol.\u00a01978, pp. 284\u2013299. Springer, Heidelberg (2001)"},{"key":"21_CR34","doi-asserted-by":"crossref","unstructured":"Kaufman, C.: Internet Key Exchange (IKEv2) Protocol, RFC (2005)","DOI":"10.17487\/rfc4306"},{"key":"21_CR35","unstructured":"Kohl, J., Neuman, B.: The kerberos network authentication service, RFC (1991)"},{"key":"21_CR36","unstructured":"Lakhnech, Y., Mazar\u00e9, L.: Computationally sound verifiation of security protocols using Diffie-Hellman exponentiation. Cryptology ePrint Archive: Report 2005\/097 (2005)"},{"issue":"1","key":"21_CR37","doi-asserted-by":"crossref","first-page":"99","DOI":"10.3233\/JCS-2004-12105","volume":"12","author":"D. Micciancio","year":"2004","unstructured":"Micciancio, D., Warinschi, B.: Completeness theorems for the Abadi-Rogaway logic of encrypted expressions. Journal of Computer Security\u00a012(1), 99\u2013129 (2004). Preliminary version in WITS 2002","journal-title":"Journal of Computer Security"},{"key":"21_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1007\/978-3-540-24638-1_8","volume-title":"Theory of Cryptography","author":"D. Micciancio","year":"2004","unstructured":"Micciancio, D., Warinschi, B.: Soundness of formal encryption in the presence of active adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol.\u00a02951, pp. 133\u2013151. Springer, Heidelberg (2004)"},{"key":"21_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-540-74835-9_15","volume-title":"Computer Security \u2013 ESORICS 2007","author":"A. Roy","year":"2007","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive proofs of computational secrecy. In: Biskup, J., L\u00f3pez, J. (eds.) ESORICS 2007. LNCS, vol.\u00a04734, pp. 219\u2013234. Springer, Heidelberg (2007), http:\/\/www.stanford.edu\/~arnab\/rddm-InductiveProofs.pdf"},{"key":"21_CR40","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive trace properties for computational security. In: WITS (2007), http:\/\/www.stanford.edu\/~arnab\/rddm-IndTraceProps.pdf"},{"key":"21_CR41","unstructured":"Roy, A., Datta, A., Derek, A., Mitchell, J.C., Seifert, J.-P.: Secrecy analysis in Protocol Composition Logic. In: Proceedings of 11th Annual Asian Computing Science Conference (to appear, 2006)"},{"key":"21_CR42","unstructured":"Roy, A., Datta, A., Mitchell, J.C.: Formal proofs of cryptographic security of Diffie-Hellman-based protocols. Manuscript (2007), http:\/\/www.stanford.edu\/~arnab\/rdm-DHProofs.pdf"},{"key":"21_CR43","doi-asserted-by":"crossref","unstructured":"Zhu, L., Tung, B.: Public Key Cryptography for Initial Authentication in Kerberos (PKINIT). RFC 4556 (Proposed Standard) (June 2006)","DOI":"10.17487\/rfc4556"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78663-4_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:17:49Z","timestamp":1619522269000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78663-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540786627","9783540786634"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78663-4_21","relation":{},"subject":[]}}