{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T22:15:47Z","timestamp":1725747347330},"publisher-location":"Berlin, Heidelberg","reference-count":38,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642411564"},{"type":"electronic","value":"9783642411571"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-41157-1_11","type":"book-chapter","created":{"date-parts":[[2013,9,4]],"date-time":"2013-09-04T14:23:39Z","timestamp":1378304619000},"page":"164-181","source":"Crossref","is-referenced-by-count":4,"title":["An Algebra for Symbolic Diffie-Hellman Protocol Analysis"],"prefix":"10.1007","author":[{"given":"Daniel J.","family":"Dougherty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joshua D.","family":"Guttman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"11_CR1","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1016\/S0304-3975(02)00090-7","volume":"290","author":"R.M. Amadio","year":"2003","unstructured":"Amadio, R.M., Lugiez, D., Vanack\u00e8re, V.: On the symbolic reduction of processes with cryptographic functions. Theoretical Computer Science\u00a0290(1), 695\u2013740 (2003)","journal-title":"Theoretical Computer Science"},{"key":"11_CR2","unstructured":"Ankney, R., Johnson, D., Matyas, M.: The Unified Model. Contribution to ANSI X9F1. Standards Projects (Financial Crypto Tools), ANSI X,\u00a042 (1995)"},{"key":"11_CR3","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.\u00a03576, pp. 281\u2013285. Springer, Heidelberg (2005)"},{"issue":"2","key":"11_CR4","doi-asserted-by":"publisher","first-page":"239","DOI":"10.2307\/1970573","volume":"88","author":"J. Ax","year":"1968","unstructured":"Ax, J.: The elementary theory of finite fields. The Annals of Mathematics\u00a088(2), 239\u2013271 (1968)","journal-title":"The Annals of Mathematics"},{"issue":"3","key":"11_CR5","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"D.A. Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: A symbolic model checker for security protocols. Int. J. Inf. Sec.\u00a04(3), 181\u2013208 (2005)","journal-title":"Int. J. Inf. Sec."},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Bergstra, J.A., Tucker, J.V.: The rational numbers as an abstract data type. Journal of the ACM\u00a054 (2007)","DOI":"10.1145\/1219092.1219095"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/3-540-48892-8_26","volume-title":"Selected Areas in Cryptography","author":"S. Blake-Wilson","year":"1999","unstructured":"Blake-Wilson, S., Menezes, A.: Authenticated Diffie-Hellman Key agreement protocols. In: Tavares, S., Meijer, H. (eds.) SAC 1998. LNCS, vol.\u00a01556, pp. 339\u2013361. Springer, Heidelberg (1999)"},{"key":"11_CR8","unstructured":"Blanchet, B.: An efficient protocol verifier based on Prolog rules. In: 14th Computer Security Foundations Workshop, pp. 82\u201396. IEEE CS Press (June 2001)"},{"key":"11_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/978-3-540-45138-9_21","volume-title":"Mathematical Foundations of Computer Science 2003","author":"M. Boreale","year":"2003","unstructured":"Boreale, M., Buscemi, M.G.: Symbolic analysis of crypto-protocols based on modular exponentiation. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 269\u2013278. Springer, Heidelberg (2003)"},{"key":"11_CR10","unstructured":"Bresson, E., Lakhnech, Y., Mazar\u00e9, L., Warinschi, B.: Computational soundness: The case of Diffie-Hellman keys. In: Cortier, V., Kremer, S. (eds.) Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series. IOS Press (2011)"},{"key":"11_CR11","unstructured":"Cervesato, I., Meadows, C., Pavlovic, D.: An encapsulated authentication logic for reasoning about key distribution protocols. In: 18th IEEE Workshop on Computer Security Foundations, CSFW-18 2005, pp. 48\u201361. IEEE (2005)"},{"key":"11_CR12","unstructured":"Chang, C.C., Keisler, H.J.: Model Theory. Studies in Logic and the Foundations of Mathematics, vol.\u00a073 (1990)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-540-24597-1_11","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"Y. Chevalier","year":"2003","unstructured":"Chevalier, Y., K\u00fcsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 124\u2013135. Springer, Heidelberg (2003)"},{"key":"11_CR14","unstructured":"Cremers, C., Feltz, M.: One-round strongly secure key exchange with perfect forward secrecy and deniability. Cryptology ePrint Archive, Report 2011\/300 (2011), http:\/\/eprint.iacr.org\/2011\/300"},{"key":"11_CR15","doi-asserted-by":"crossref","unstructured":"Cremers, C., Schmidt, B., Meier, S., Basin, D.: Automated analysis of Diffie-Hellman protocols and advanced security properties. In: Computer Security Foundations (CSF) (2012)","DOI":"10.1109\/CSF.2012.25"},{"key":"11_CR16","unstructured":"Cremers, C.J.F.: Scyther - Semantics and Verification of Security Protocols. Ph.D. dissertation, Eindhoven University of Technology (2006)"},{"issue":"6","key":"11_CR17","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 Transactions on Information Theory\u00a022(6), 644\u2013654 (1976)","journal-title":"IEEE Transactions on Information Theory"},{"key":"11_CR18","unstructured":"Dougherty, D.J., Guttman, J.D.: Symbolic protocol analysis for Diffie-Hellman, Arxiv preprint arXiv:1202.2168 (2012), http:\/\/arxiv.org\/abs\/1202.2168v1"},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-642-16310-4_6","volume-title":"Rewriting Logic and Its Applications","author":"F. Dur\u00e1n","year":"2010","unstructured":"Dur\u00e1n, F., Meseguer, J.: A church-Rosser checker tool for conditional order-sorted equational maude specifications. In: \u00d6lveczky, P.C. (ed.) WRLA 2010. LNCS, vol.\u00a06381, pp. 69\u201385. Springer, Heidelberg (2010), Version 3j, available at http:\/\/maude.lcc.uma.es\/CRChC"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/978-3-540-88313-5_35","volume-title":"Computer Security - ESORICS 2008","author":"S. Escobar","year":"2008","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: State space reduction in the Maude-NRL protocol analyzer. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol.\u00a05283, pp. 548\u2013562. Springer, Heidelberg (2008)"},{"key":"11_CR21","series-title":"LNCS","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\/2008\/2009. LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Heidelberg (2009)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Fiore, M., Abadi, M.: Computing symbolic models for verifying cryptographic protocols. In: Computer Security Foundations Workshop (June 2001)","DOI":"10.1109\/CSFW.2001.930144"},{"key":"11_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/11814771_24","volume-title":"Automated Reasoning","author":"J. Giesl","year":"2006","unstructured":"Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: automatic termination proofs in the dependency pair framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 281\u2013286. Springer, Heidelberg (2006)"},{"issue":"2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/j.jlap.2004.09.004","volume":"64","author":"J. Goubault-Larrecq","year":"2005","unstructured":"Goubault-Larrecq, J., Roger, M., Verma, K.: Abstraction and resolution modulo AC: How to verify Diffie-Hellman-like protocols automatically. Journal of Logic and Algebraic Programming\u00a064(2), 219\u2013251 (2005)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"11_CR25","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)"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Guttman, J.D.: State and progress in strand spaces: Proving fair exchange. Journal of Automated Reasoning (March 2010) (accepted), doi:10.1007\/s10817-010-9202-1","DOI":"10.1007\/s10817-010-9202-1"},{"issue":"3","key":"11_CR27","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1145\/501978.501981","volume":"4","author":"B.S. Kaliski","year":"2001","unstructured":"Kaliski, B.S.: An unknown key-share attack on the MQV key agreement protocol. ACM Transactions on Information and System Security\u00a04(3), 275\u2013288 (2001)","journal-title":"ACM Transactions on Information and System Security"},{"key":"11_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/3-540-44881-0_13","volume-title":"Rewriting Techniques and Applications","author":"D. Kapur","year":"2003","unstructured":"Kapur, D., Narendran, P., Wang, L.: An E-unification algorithm for analyzing protocols that use modular exponentiation. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 165\u2013179. Springer, Heidelberg (2003)"},{"key":"11_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/11535218_33","volume-title":"Advances in Cryptology \u2013 CRYPTO 2005","author":"H. Krawczyk","year":"2005","unstructured":"Krawczyk, H.: HMQV: A high-performance secure Diffie-Hellman protocol. In: Shoup, V. (ed.) CRYPTO 2005. LNCS, vol.\u00a03621, pp. 546\u2013566. Springer, Heidelberg (2005)"},{"key":"11_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/11832072_11","volume-title":"Security and Cryptography for Networks","author":"S. Kunz-Jacques","year":"2006","unstructured":"Kunz-Jacques, S., Pointcheval, D.: About the Security of MTI\/C0 and MQV. In: De Prisco, R., Yung, M. (eds.) SCN 2006. LNCS, vol.\u00a04116, pp. 156\u2013172. Springer, Heidelberg (2006)"},{"key":"11_CR31","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"},{"issue":"2","key":"11_CR32","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1023\/A:1022595222606","volume":"28","author":"L. Law","year":"2003","unstructured":"Law, L., Menezes, A., Qu, M., Solinas, J., Vanstone, S.: An efficient protocol for authenticated key agreement. Designs, Codes and Cryptography\u00a028(2), 119\u2013134 (2003)","journal-title":"Designs, Codes and Cryptography"},{"key":"11_CR33","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1515\/JMC.2007.004","volume":"1","author":"A. Menezes","year":"2007","unstructured":"Menezes, A.: Another look at HMQV. Journal of Mathematical Cryptology\u00a01, 47\u201364 (2007)","journal-title":"Journal of Mathematical Cryptology"},{"key":"11_CR34","doi-asserted-by":"crossref","unstructured":"Millen, J.K., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: 8th ACM Conference on Computer and Communications Security (CCS 2001), pp. 166\u2013175. ACM (2001)","DOI":"10.1145\/501983.502007"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/11863908_24","volume-title":"Computer Security \u2013 ESORICS 2006","author":"D. Pavlovic","year":"2006","unstructured":"Pavlovic, D., Meadows, C.: Deriving secrecy in key establishment protocols. In: Gollmann, D., Meier, J., Sabelfeld, A. (eds.) ESORICS 2006. LNCS, vol.\u00a04189, pp. 384\u2013403. Springer, Heidelberg (2006)"},{"key":"11_CR36","unstructured":"Ramsdell, J.D., Guttman, J.D.: CPSA: A cryptographic protocol shapes analyzer. In: Hackage. The MITRE Corporation (2009), http:\/\/hackage.haskell.org\/package\/cpsa ; see esp. doc subdirectory"},{"key":"11_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/3-540-48685-2_11","volume-title":"Rewriting Techniques and Applications","author":"A. Rubio","year":"1999","unstructured":"Rubio, A.: A fully syntactic AC-RPO. In: Narendran, P., Rusinowitch, M. (eds.) RTA 1999. LNCS, vol.\u00a01631, pp. 133\u2013147. Springer, Heidelberg (1999)"},{"issue":"2\/3","key":"11_CR38","doi-asserted-by":"crossref","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. Journal of Computer Security\u00a07(2\/3), 191\u2013230 (1999)","journal-title":"Journal of Computer Security"}],"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-642-41157-1_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,5]],"date-time":"2022-03-05T14:38:34Z","timestamp":1646491114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-41157-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642411564","9783642411571"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-41157-1_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}