{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T10:31:25Z","timestamp":1774434685396,"version":"3.50.1"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032206831","type":"print"},{"value":"9783032206848","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-20684-8_5","type":"book-chapter","created":{"date-parts":[[2026,3,16]],"date-time":"2026-03-16T14:07:23Z","timestamp":1773670043000},"page":"73-97","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Treatment of\u00a0the\u00a0Limits of\u00a0Authenticated Key Exchange Security"],"prefix":"10.1007","author":[{"given":"Mich\u00e8le","family":"Feltz","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0322-2293","authenticated-orcid":false,"given":"Cas","family":"Cremers","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,3,17]]},"reference":[{"key":"5_CR1","unstructured":"Alwen, J., Coretti, S., Dodis, Y.: The Double Ratchet: Security Notions, Proofs, and Modularization for the Signal Protocol. Cryptology ePrint Archive, Paper 2018\/1037 (2018). https:\/\/eprint.iacr.org\/2018\/1037"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Basin, D., Cremers, C.: Degrees of security: Protocol guarantees in the face of compromising adversaries. In: Computer Science Logic, 24th International Workshop, CSL 2010, 19th Annual Conference of the EACSL. LNCS, vol.\u00a06247. Springer(2010)","DOI":"10.1007\/978-3-642-15205-4_1"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated key exchange secure against dictionary attacks. In: 19th International Conference on Theory and Application of Cryptographic Techniques, pp. 139\u2013155. EUROCRYPT\u201900, Springer (2000)","DOI":"10.1007\/3-540-45539-6_11"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Entity authentication and key distribution. In: 13th Annual International Cryptology Conference on Advances in Cryptology, pp. 232\u2013249. CRYPTO \u201993, Springer New York, NY, USA (1994)","DOI":"10.1007\/3-540-48329-2_21"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Provably secure session key distribution: the three party case. In: 27th Annual ACM Symposium on Theory of computing, pp. 57\u201366. STOC \u201995, ACM New York, NY, USA (1995)","DOI":"10.1145\/225058.225084"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/BFb0024447","volume-title":"Crytography and Coding","author":"S Blake-Wilson","year":"1997","unstructured":"Blake-Wilson, S., Johnson, D., Menezes, A.: Key agreement protocols and their security analysis. In: Darnell, M. (ed.) Cryptography and Coding 1997. LNCS, vol. 1355, pp. 30\u201345. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0024447"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Blake-Wilson, S., Menezes, A.: Unknown key-share attacks on the Station-to-Station (STS) protocol. In: Proceedings of the Second International Workshop on Practice and Theory in Public Key Cryptography. LNCS, vol.\u00a01560. Springer (1999)","DOI":"10.1007\/3-540-49162-7_12"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/978-3-642-40203-6_22","volume-title":"Computer Security \u2013 ESORICS 2013","author":"C Boyd","year":"2013","unstructured":"Boyd, C., Cremers, C., Feltz, M., Paterson, K.G., Poettering, B., Stebila, D.: ASICS: Authenticated Key Exchange Security Incorporating Certification Systems. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 381\u2013399. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40203-6_22"},{"key":"5_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/978-3-642-25516-8_27","volume-title":"Cryptography and Coding","author":"C Boyd","year":"2011","unstructured":"Boyd, C., Nieto, J.G.: On forward secrecy in one-round key exchange. In: Chen, L. (ed.) IMACC 2011. LNCS, vol. 7089, pp. 451\u2013468. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25516-8_27"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Brzuska, C., Fischlin, M., Warinschi, B., Williams, S.: Composability of Bellare-Rogaway key exchange protocols. In: Proceedings of the 18th ACM conference on Computer and communications security, pp. 51\u201362. CCS \u201911, ACM (2011)","DOI":"10.1145\/2046707.2046716"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Canetti, R., Krawczyk, H.: Analysis of key-exchange protocols and their use for building secure channels. In: EUROCRYPT\u201901. LNCS, vol.\u00a02045, pp. 453\u2013474. Springer London, UK (2001)","DOI":"10.1007\/3-540-44987-6_28"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-02617-1_14","volume-title":"Advances in Information Security and Assurance","author":"Q Cheng","year":"2009","unstructured":"Cheng, Q., Ma, C., Hu, X.: A new strongly secure authenticated key exchange protocol. In: Park, J.H., Chen, H.-H., Atiquzzaman, M., Lee, C., Kim, T., Yeo, S.-S. (eds.) ISA 2009. LNCS, vol. 5576, pp. 135\u2013144. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02617-1_14"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"Choo, K.K.R., Boyd, C., Hitchcock, Y.: Examining indistinguishability-based proof models for key establishment protocols. In: Proceedings of the 11th international conference on Theory and Application of Cryptology and Information Security. ASIACRYPT\u201905, Springer-Verlag (2005)","DOI":"10.1007\/11593447_32"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/978-3-540-75496-1_14","volume-title":"Information Security","author":"SSM Chow","year":"2007","unstructured":"Chow, S.S.M., Choo, K.-K.R.: Strongly-secure identity-based key agreement and anonymous extension. In: Garay, J.A., Lenstra, A.K., Mambo, M., Peralta, R. (eds.) ISC 2007. LNCS, vol. 4779, pp. 203\u2013220. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75496-1_14"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"Cohn-Gordon, K., Cremers, C.J.F., Garratt, L.: On post-compromise security. In: CSF, pp. 164\u2013178. IEEE Computer Society (2016)","DOI":"10.1109\/CSF.2016.19"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"Cremers, C.: Examining indistinguishability-based security models for key exchange protocols: the case of CK, CK-HMQV, and eCK. In: Proceedings of ACM Symposium on Information, Computer and Communications Security. ASIACCS \u201911, ACM (2011)","DOI":"10.1145\/1966913.1966925"},{"key":"5_CR17","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":"5_CR18","doi-asserted-by":"crossref","unstructured":"Cremers, C., Feltz, M.: Beyond eCK: perfect forward secrecy under actor compromise and ephemeral-key reveal. In: Proceedings of the 17th European Conference on Research in Computer Security. ESORICS, Springer-Verlag (2012)","DOI":"10.1007\/978-3-642-33167-1_42"},{"key":"5_CR19","volume-title":"Beyond eCK: Perfect Forward Secrecy Under Actor Compromise and Ephemeral-key Reveal","author":"C Cremers","year":"2013","unstructured":"Cremers, C., Feltz, M.: Beyond eCK: Perfect Forward Secrecy Under Actor Compromise and Ephemeral-key Reveal. Designs, Codes and Cryptography (2013)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Cremers, C., Feltz, M.: Beyond eCK: Perfect Forward Secrecy under Actor Compromise and Ephemeral-Key Reveal. Cryptology ePrint Archive, Report 2012\/416 (2012). http:\/\/eprint.iacr.org\/2012\/416","DOI":"10.1007\/978-3-642-33167-1_42"},{"key":"5_CR21","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, Information Security and Cryptography (2012)"},{"key":"5_CR22","unstructured":"Engels, A., Mauw, S.: Why men (and octopuses) cannot juggle a four ball cascade (1997). https:\/\/satoss.uni.lu\/members\/sjouke\/papers\/EnMa02.pdf"},{"key":"5_CR23","doi-asserted-by":"publisher","unstructured":"Feltz, M., Cremers, C.: Strengthening the security of authenticated key exchange against bad randomness. Designs, Codes Cryptograph. 86(3), 481\u2013516 (Mar 2018). https:\/\/doi.org\/10.1007\/s10623-017-0337-5","DOI":"10.1007\/s10623-017-0337-5"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"Feltz, M., Cremers, C.: A Formal Treatment of the Limits of Key Exchange Security (Long Version) (2025). https:\/\/people.cispa.io\/cas.cremers\/downloads\/papers\/akelimits-SMLXV-long.pdf","DOI":"10.1007\/978-3-032-20684-8_5"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"Gennaro, R., Krawczyk, H., Rabin, T.: Okamoto-Tanaka revisited: fully authenticated Diffie-Hellman with minimal overhead. In: ACNS\u201910. Springer (2010)","DOI":"10.1007\/978-3-642-13708-2_19"},{"key":"5_CR26","doi-asserted-by":"crossref","unstructured":"Hao, F.: On robust key agreement based on public key authentication. In: Financial Cryptography. LNCS, vol.\u00a06052, pp. 383\u2013390. Springer (2010)","DOI":"10.1007\/978-3-642-14577-3_33"},{"key":"5_CR27","doi-asserted-by":"crossref","unstructured":"Kim, M., Fujioka, A., Ustaoglu, B.: Strongly secure authenticated key exchange without NAXOS\u2019 approach. In: IWSEC\u201909, pp. 174\u2013191 (2009)","DOI":"10.1007\/978-3-642-04846-3_12"},{"key":"5_CR28","doi-asserted-by":"crossref","unstructured":"Krawczyk, H.: SIGMA: The \u2019SIGn-and-MAc\u2019 approach to authenticated Diffie-Hellman and its use in the IKE-Protocols. In: CRYPTO, pp. 400\u2013425 (2003)","DOI":"10.1007\/978-3-540-45146-4_24"},{"key":"5_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. 3621, pp. 546\u2013566. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11535218_33"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"Krawczyk, H.: HMQV: A High-Performance Secure Diffie-Hellman Protocol. Cryptology ePrint Archive, Report 2005\/176 (2005). http:\/\/eprint.iacr.org\/2005\/176","DOI":"10.1007\/11535218_33"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-75670-5_1","volume-title":"Provable Security","author":"B LaMacchia","year":"2007","unstructured":"LaMacchia, B., Lauter, K., Mityagin, A.: Stronger security of authenticated key exchange. In: Susilo, W., Liu, J.K., Mu, Y. (eds.) ProvSec 2007. LNCS, vol. 4784, pp. 1\u201316. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75670-5_1"},{"key":"5_CR32","unstructured":"Lee, J., Park, J.: Authenticated key exchange secure under the computational Diffie-Hellman assumption. Cryptology ePrint Archive, Report 2008\/344 (2008). https:\/\/eprint.iacr.org\/2008\/344"},{"key":"5_CR33","doi-asserted-by":"crossref","unstructured":"Lysyanskaya, A.: Unique signatures and verifiable random functions from the DH-DDH separation, pp. 597\u2013612. Springer Berlin Heidelberg (2002)","DOI":"10.1007\/3-540-45708-9_38"},{"key":"5_CR34","volume-title":"Handbook of Applied Cryptography","author":"A Menezes","year":"1996","unstructured":"Menezes, A., van Oorschot, P., Vanstone, S.: Handbook of Applied Cryptography. CRC Press, Boca Raton, FL, USA (1996)"},{"key":"5_CR35","unstructured":"Poettering, B., R\u00f6sler, P.: Asynchronous ratcheted key exchange. Cryptology ePrint Archive, Report 2018\/296 (2018). https:\/\/eprint.iacr.org\/2018\/296"},{"key":"5_CR36","doi-asserted-by":"crossref","unstructured":"Sarr, A., Elbaz-Vincent, P., Bajard, J.C.: A new security model for authenticated key agreement. Secur. Cryptograph. Netw. 219\u2013234 (2010)","DOI":"10.1007\/978-3-642-15317-4_15"},{"key":"5_CR37","doi-asserted-by":"crossref","unstructured":"Sch\u00e4ge, S.: TOPAS: 2-pass key exchange with full perfect forward secrecy and optimal communication complexity. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pp. 1224\u20131235. ACM (2015)","DOI":"10.1145\/2810103.2813683"},{"key":"5_CR38","unstructured":"Ustaoglu, B.: Obtaining a secure and efficient key agreement protocol from (H)MQV and NAXOS. Cryptology ePrint Archive, Report 2007\/123 (2007), https:\/\/eprint.iacr.org\/2007\/123"},{"key":"5_CR39","doi-asserted-by":"crossref","unstructured":"Yang, G., Duan, S., Wong, D.S., Tan, C.H., Wang, H.: Authenticated key exchange under bad randomness. In: Proceedings of the 15th International Conference on Financial Cryptography and Data Security, pp. 113\u2013126. FC\u201911, Springer-Verlag (2012)","DOI":"10.1007\/978-3-642-27576-0_10"}],"container-title":["Lecture Notes in Computer Science","Juggling Formal Methods and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-20684-8_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T23:01:53Z","timestamp":1774393313000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-20684-8_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032206831","9783032206848"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-20684-8_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"17 March 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}}]}}