{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T04:33:00Z","timestamp":1726029180058},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030190514"},{"type":"electronic","value":"9783030190521"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-19052-1_10","type":"book-chapter","created":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T01:11:42Z","timestamp":1558573902000},"page":"135-155","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Enrich-by-Need Protocol Analysis for Diffie-Hellman"],"prefix":"10.1007","author":[{"given":"Moses D.","family":"Liskov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua D.","family":"Guttman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John D.","family":"Ramsdell","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul D.","family":"Rowe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"F. Javier","family":"Thayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,4,28]]},"reference":[{"key":"10_CR1","unstructured":"Ankney, R., Johnson, D., Matyas, M.: The Unified Model. Contribution to ANSI X9F1. Standards Projects (Financial Crypto Tools), ANSI X, 42 (1995)"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11513988_27","volume-title":"Computer Aided Verification","author":"A Armando","year":"2005","unstructured":"Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281\u2013285. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_27"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-662-44371-2_6","volume-title":"Advances in Cryptology \u2013 CRYPTO 2014","author":"G Barthe","year":"2014","unstructured":"Barthe, G., Fagerholm, E., Fiore, D., Mitchell, J.C., Scedrov, A., Schmidt, B.: Automated analysis of cryptographic assumptions in generic group models. In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014. LNCS, vol. 8616, pp. 95\u2013112. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44371-2_6"},{"issue":"6","key":"10_CR4","doi-asserted-by":"publisher","first-page":"817","DOI":"10.3233\/JCS-130472","volume":"21","author":"DA Basin","year":"2013","unstructured":"Basin, D.A., Cremers, C., Meier, S.: Provably repairing the ISO\/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817\u2013846 (2013)","journal-title":"J. Comput. Secur."},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-48329-2_21","volume-title":"Advances in Cryptology \u2014 CRYPTO 93","author":"M Bellare","year":"1994","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: Stinson, D.R. (ed.) CRYPTO 1993. LNCS, vol. 773, pp. 232\u2013249. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-48329-2_21"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/978-3-642-23822-2_18","volume-title":"Computer Security \u2013 ESORICS 2011","author":"C Cremers","year":"2011","unstructured":"Cremers, C.: Key exchange in IPsec revisited: formal analysis of IKEv1 and IKEv2. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 315\u2013334. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-23822-2_18"},{"key":"10_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78636-8","volume-title":"Operational Semantics and Verification of Security Protocols","author":"C Cremers","year":"2012","unstructured":"Cremers, C., Mauw, S.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-540-78636-8"},{"issue":"6","key":"10_CR8","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Trans. Inf. Theory 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"2","key":"10_CR9","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/BF00124891","volume":"2","author":"W Diffie","year":"1992","unstructured":"Diffie, W., van Oorschot, P.C., Wiener, M.J.: Authentication and authenticated key exchanges. Des. Codes Cryptogr. 2(2), 107\u2013125 (1992)","journal-title":"Des. Codes Cryptogr."},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.: On the security of public-key protocols. IEEE Trans. Inf. Theory 29, 198\u2013208 (1983)","journal-title":"IEEE Trans. Inf. Theory"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Dougherty, D.J., Guttman, J.D.: Decidability for lightweight Diffie-Hellman protocols. In: IEEE Symposium on Computer Security Foundations (2014)","DOI":"10.1109\/CSF.2014.23"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-03829-7_1","volume-title":"Foundations of Security Analysis and Design V","author":"S Escobar","year":"2009","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1\u201350. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1"},{"key":"10_CR13","unstructured":"Guttman, J.D.: Shapes: surveying crypto protocol runs. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols, Cryptology and Information Security Series. IOS Press (2011)"},{"issue":"2","key":"10_CR14","doi-asserted-by":"publisher","first-page":"201","DOI":"10.3233\/JCS-140497","volume":"22","author":"JD Guttman","year":"2014","unstructured":"Guttman, J.D.: Establishing and preserving protocol security goals. J. Comput. Secur. 22(2), 201\u2013267 (2014)","journal-title":"J. Comput. Secur."},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"K\u00fcsters, R., Truderung, T.: Using ProVerif to analyze protocols with Diffie-Hellman exponentiation. In: IEEE Computer Security Foundations Symposium, pp. 157\u2013171. IEEE (2009)","DOI":"10.1109\/CSF.2009.17"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Liskov, M., Javier Thayer, F.: Modeling Diffie-Hellman derivability for automated analysis. In: IEEE Computer Security Foundations, pp. 232\u2013243 (2014)","DOI":"10.1109\/CSF.2014.24"},{"key":"10_CR17","doi-asserted-by":"crossref","unstructured":"Liskov, M.D., Guttman, J.D., Ramsdell, J.D., Rowe, P.D., Javier Thayer, F.: Enrich-by-need protocol analysis for Diffie-Hellman (extended version), April 2018. http:\/\/arxiv.org\/abs\/1804.05713","DOI":"10.1007\/978-3-030-19052-1_10"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Liskov, M.D., Rowe, P.D., Javier Thayer, F.: Completeness of CPSA. Technical Report MTR110479, The MITRE Corporation, March 2011. http:\/\/www.mitre.org\/publications\/technical-papers\/completeness-of-cpsa","DOI":"10.21236\/ADA562264"},{"key":"10_CR19","doi-asserted-by":"crossref","unstructured":"Liskov, M.D., Javier Thayer, F.: Formal modeling of Diffie-Hellman derivability for exploratory automated analysis. Technical report, MITRE, June 2013. TR 13\u20130411","DOI":"10.1109\/CSF.2014.24"},{"key":"10_CR20","unstructured":"Lowe, G.: A hierarchy of authentication specifications. In: 10th Computer Security Foundations Workshop Proceedings, pp. 31\u201343. IEEE CS Press (1997)"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11586821_1","volume-title":"Cryptography and Coding","author":"UM Maurer","year":"2005","unstructured":"Maurer, U.M.: Abstract models of computation in cryptography. In: Smart, N.P. (ed.) Cryptography and Coding 2005. LNCS, vol. 3796, pp. 1\u201312. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11586821_1"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"696","DOI":"10.1007\/978-3-642-39799-8_48","volume-title":"Computer Aided Verification","author":"S Meier","year":"2013","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696\u2013701. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48"},{"key":"10_CR23","unstructured":"Ramsdell, J.D.: Deducing security goals from shape analysis sentences. The MITRE Corporation, April 2012. http:\/\/arxiv.org\/abs\/1204.0480"},{"key":"10_CR24","unstructured":"Ramsdell, J.D., Guttman, J.D.: CPSA: a cryptographic protocol shapes analyzer (2009). http:\/\/hackage.haskell.org\/package\/cpsa"},{"key":"10_CR25","doi-asserted-by":"publisher","unstructured":"Rowe, P.D., Guttman, J.D., Liskov, M.D.: Measuring protocol strength with security goals. Int. J. Inf. Secur. 15(6), 575\u2013596 (2016). https:\/\/doi.org\/10.1007\/s10207-016-0319-z . http:\/\/web.cs.wpi.edu\/~guttman\/pubs\/ijis_measuring-security.pdf","DOI":"10.1007\/s10207-016-0319-z"},{"key":"10_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/3-540-69053-0_18","volume-title":"Advances in Cryptology \u2014 EUROCRYPT 97","author":"V Shoup","year":"1997","unstructured":"Shoup, V.: Lower bounds for discrete logarithms and related problems. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 256\u2013266. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-69053-0_18"},{"issue":"2\/3","key":"10_CR27","doi-asserted-by":"publisher","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F Javier Thayer","year":"1999","unstructured":"Javier Thayer, F., Herzog, J.C., Guttman, J.D.: Strand spaces: proving security protocols correct. J. Comput. Secur. 7(2\/3), 191\u2013230 (1999)","journal-title":"J. Comput. Secur."},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/11805618_21","volume-title":"Term Rewriting and Applications","author":"M Turuani","year":"2006","unstructured":"Turuani, M.: The CL-Atse protocol analyser. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 277\u2013286. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11805618_21"},{"key":"10_CR29","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2005.11.052","volume":"155","author":"L Vigan\u00f2","year":"2006","unstructured":"Vigan\u00f2, L.: Automated security protocol analysis with the AVISPA tool. Electron. Notes Theor. Comput. Sci. 155, 61\u201386 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Foundations of Security, Protocols, and Equational Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-19052-1_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,18]],"date-time":"2022-09-18T12:58:57Z","timestamp":1663505937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-19052-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030190514","9783030190521"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-19052-1_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}