{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T03:02:38Z","timestamp":1779850958056,"version":"3.53.1"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032078902","type":"print"},{"value":"9783032078919","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,17]],"date-time":"2025-10-17T00:00:00Z","timestamp":1760659200000},"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-07891-9_10","type":"book-chapter","created":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T10:23:49Z","timestamp":1760610229000},"page":"186-204","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Symbolic Analysis of\u00a0Hash Functions Vulnerabilities in\u00a0Maude-NPA"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0000-2955-3045","authenticated-orcid":false,"given":"Arturo","family":"Hern\u00e1ndez-S\u00e1nchez","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3550-4781","authenticated-orcid":false,"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2025,10,17]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-030-59013-0_12","volume-title":"Computer Security \u2013 ESORICS 2020","author":"D Aparicio-S\u00e1nchez","year":"2020","unstructured":"Aparicio-S\u00e1nchez, D., Escobar, S., Guti\u00e9rrez, R., Sapi\u00f1a, J.: An optimizing protocol transformation for constructor finite variant theories in Maude-NPA. In: Chen, L., Li, N., Liang, K., Schneider, S. (eds.) ESORICS 2020. LNCS, vol. 12309, pp. 230\u2013250. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59013-0_12"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Aparicio-S\u00e1nchez, D., Escobar, S., Meadows, C., Meseguer, J., Sapi\u00f1a, J.: Protocol analysis with time and space. In: Protocols, Strands, and Logic: Essays Dedicated to Joshua Guttman on the Occasion of his 66.66 th Birthday, pp. 22\u201349. Springer (2021)","DOI":"10.1007\/978-3-030-91631-2_2"},{"key":"10_CR3","unstructured":"Aurora, V.: Lifetimes of cryptographic hash functions (2017). https:\/\/valerieaurora.org\/hash.html"},{"key":"10_CR4","doi-asserted-by":"publisher","unstructured":"Bellare, M., Canetti, R., Krawczyk, H.: Keying hash functions for message authentication. In: Koblitz, N. (ed.) CRYPTO 1996. LNCS, vol. 1109, pp. 1\u201315. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/3-540-68697-5_1","DOI":"10.1007\/3-540-68697-5_1"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: Proceedings of the 1st ACM Conference on Computer and Communications Security, pp. 62\u201373 (1993)","DOI":"10.1145\/168588.168596"},{"key":"10_CR6","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Leurent, G.: Transcript collision attacks: breaking authentication in TLS, IKE, and SSH. In: Network and Distributed System Security Symposium\u2013NDSS 2016 (2016)","DOI":"10.14722\/ndss.2016.23418"},{"key":"10_CR7","doi-asserted-by":"publisher","unstructured":"Blanchet, B., Cheval, V., Cortier, V.: Proverif with lemmas, induction, fast subsumption, and much more. In: 43rd IEEE Symposium on Security and Privacy, SP 2022, San Francisco, CA, USA, May 22-26, 2022, pp. 69\u201386. IEEE (2022). https:\/\/doi.org\/10.1109\/SP46214.2022.9833653","DOI":"10.1109\/SP46214.2022.9833653"},{"key":"10_CR8","unstructured":"Cheval, V., Cremers, C., Dax, A., Hirschi, L., Jacomme, C., Kremer, S.: Hash gone bad: automated discovery of protocol attacks that exploit hash function weaknesses. In: 32nd USENIX Security Symposium (USENIX Security 23), pp. 5899\u20135916 (2023)"},{"key":"10_CR9","unstructured":"Clavel, M., et al.: Maude manual (version 3.5) (2024). http:\/\/maude.cs.uiuc.edu"},{"key":"10_CR10","doi-asserted-by":"publisher","unstructured":"Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Proceedings of the 16th International Conference on Rewriting Techniques and Applications (RTA 2005). LNCS, vol.\u00a03467, pp. 294\u2013307. Springer (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_22","DOI":"10.1007\/978-3-540-32033-3_22"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Damg\u00e5rd, I.B.: A design principle for hash functions. In: Conference on the Theory and Application of Cryptology, pp. 416\u2013427. Springer (1989)","DOI":"10.1007\/0-387-34805-0_39"},{"key":"10_CR12","doi-asserted-by":"crossref","unstructured":"Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.2, Technical report (2008)","DOI":"10.17487\/rfc5246"},{"issue":"6","key":"10_CR13","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1109\/C-M.1977.217750","volume":"10","author":"W Diffie","year":"1997","unstructured":"Diffie, W., Hellman, M.: Exhaustive cryptanalysis of the NBS data encryption standard. Computer 10(6), 74\u201384 (1997)","journal-title":"Computer"},{"key":"10_CR14","unstructured":"Duong, T., Rizzo, J.: Flickr\u2019s API signature forgery vulnerability, Technical report (2009)"},{"key":"10_CR15","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., et al.: Programming and symbolic computation in Maude. J. Log. Algebraic Methods Program. 110 (2020). https:\/\/doi.org\/10.1016\/J.JLAMP.2019.100497","DOI":"10.1016\/J.JLAMP.2019.100497"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Dur\u00e1n, F., Eker, S., Escobar, S., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: Associative unification and symbolic reasoning modulo associativity in Maude. In: Rusu, V. (ed.) Rewriting Logic and Its Applications - 12th International Workshop, WRLA 2018, Held as a Satellite Event of ETAPS, Thessaloniki, Greece, June 14\u201315, 2018, Proceedings. LNCS, vol. 11152, pp. 98\u2013114. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-99840-4_6","DOI":"10.1007\/978-3-319-99840-4_6"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"100747","DOI":"10.1016\/J.JLAMP.2021.100747","volume":"126","author":"S Eker","year":"2022","unstructured":"Eker, S.: Associative unification in Maude. J. Log. Algebraic Methods Program. 126, 100747 (2022). https:\/\/doi.org\/10.1016\/J.JLAMP.2021.100747","journal-title":"J. Log. Algebraic Methods Program."},{"key":"10_CR18","unstructured":"Escobar, S., Hendrix, J., Meadows, C., Meseguer, J.: Diffie-Hellman cryptographic reasoning in the Maude-NRL protocol analyzer. In: Proceedings of the 2nd International Workshop on Security and Rewriting Techniques (SecReT 2007) (2007)"},{"key":"10_CR19","doi-asserted-by":"publisher","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Foundations of Security Analysis and Design V (FOSAD 2007\/2008\/2009 Tutorial Lectures). LNCS, vol.\u00a05705, pp. 1\u201350. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-03829-7_1","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2008\/2009 Tutorial Lectures. LNCS, vol.\u00a05705, pp. 1\u201350. Springer (2009)","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"10_CR21","doi-asserted-by":"publisher","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: Symbolic protocol analysis with disequality constraints modulo equational theories. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security: Essays Dedicated to Pierpaolo Degano on the Occasion of his 65th Birthday. LNCS, vol. 9465, pp. 238\u2013261. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25527-9_16","DOI":"10.1007\/978-3-319-25527-9_16"},{"key":"10_CR22","doi-asserted-by":"publisher","unstructured":"Escobar, S., et al.: Protocol analysis in Maude-NPA using unification modulo homomorphic encryption. In: Schneider-Kamp, P., Hanus, M. (eds.) Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 20\u201322, 2011, Odense, Denmark, pp. 65\u201376. ACM (2011). https:\/\/doi.org\/10.1145\/2003476.2003488","DOI":"10.1145\/2003476.2003488"},{"key":"10_CR23","unstructured":"Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA manual v3.1. http:\/\/maude.cs.illinois.edu\/w\/index.php\/Maude_Tools:_Maude-NPA"},{"key":"10_CR24","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1016\/j.ic.2014.07.007","volume":"238","author":"S Escobar","year":"2014","unstructured":"Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: State space reduction in the Maude-NRL protocol analyzer. Inf. Comput. 238, 157\u2013186 (2014). https:\/\/doi.org\/10.1016\/j.ic.2014.07.007","journal-title":"Inf. Comput."},{"issue":"7\u20138","key":"10_CR25","doi-asserted-by":"publisher","first-page":"898","DOI":"10.1016\/j.jlap.2012.01.002","volume":"81","author":"S Escobar","year":"2012","unstructured":"Escobar, S., Sasse, R., Meseguer, J.: Folding variant narrowing and optimal variant termination. J. Log. Algebr. Program. 81(7\u20138), 898\u2013928 (2012). https:\/\/doi.org\/10.1016\/j.jlap.2012.01.002","journal-title":"J. Log. Algebr. Program."},{"key":"10_CR26","doi-asserted-by":"publisher","unstructured":"Fabrega, F.J.T., Herzog, J.C., Guttman, J.D.: Strand spaces: why is a security protocol correct? In: Proceedings. In: 1998 IEEE Symposium on Security and Privacy (Cat. No.98CB36186), pp. 160\u2013171 (1998). https:\/\/doi.org\/10.1109\/SECPRI.1998.674832","DOI":"10.1109\/SECPRI.1998.674832"},{"key":"10_CR27","unstructured":"Hern\u00e1ndez-S\u00e1nchez, A., Escobar, S.: Hash vulnerabilities analysis in Maude-NPA (2025). https:\/\/personales.upv.es\/sanesro\/Maude-NPA_Protocols\/Hash"},{"key":"10_CR28","doi-asserted-by":"crossref","unstructured":"Katz, J., Lindell, Y.: Introduction to Modern Cryptography: Principles and Protocols. Chapman and Hall\/CRC (2007)","DOI":"10.1201\/9781420010756"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Krawczyk, H.: Sigma: the \u2018sign-and-mac\u2019 approach to authenticated Diffie-Hellman and its use in the IKE protocols. In: Annual International Cryptology Conference, pp. 400\u2013425. Springer (2003)","DOI":"10.1007\/978-3-540-45146-4_24"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Meadows, C., Poovendran, R., Pavlovic, D., Chang, L., Syverson, P.: Distance bounding protocols: authentication logic analysis and collusion attacks. In: Secure Localization and Time Synchronization for Wireless Sensor and Ad Hoc Networks, pp. 279\u2013298. Springer (2007)","DOI":"10.1007\/978-0-387-46276-9_12"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Merkle, R.C.: One way hash functions and des. In: Conference on the Theory and Application of Cryptology, pp. 428\u2013446. Springer (1989)","DOI":"10.1007\/0-387-34805-0_40"},{"issue":"1","key":"10_CR32","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci. 96(1), 73\u2013155 (1992)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR33","unstructured":"National Institute of Standards and Technology (NIST): Secure Hash Standard (SHS) - FIPS PUB 180-4, Technical Report FIPS PUB 180-4, NIST (2015). https:\/\/nvlpubs.nist.gov\/nistpubs\/FIPS\/NIST.FIPS.180-4.pdf"},{"key":"10_CR34","doi-asserted-by":"publisher","unstructured":"Rivest, R.L.: The MD5 message-digest algorithm. RFC 1321 (1992). https:\/\/doi.org\/10.17487\/RFC1321","DOI":"10.17487\/RFC1321"},{"key":"10_CR35","unstructured":"Rivest, R.L.: The MD4 message digest algorithm. LNCS, Advances in Cryptography CRYPTO \u201990 (1998)"},{"key":"10_CR36","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-22444-7_11","volume-title":"Security and Trust Management","author":"R Sasse","year":"2011","unstructured":"Sasse, R., Escobar, S., Meadows, C., Meseguer, J.: Protocol analysis modulo combination of theories: a case study in Maude-NPA. In: Cuellar, J., Lopez, J., Barthe, G., Pretschner, A. (eds.) Security and Trust Management, pp. 163\u2013178. Springer, Berlin, Heidelberg (2011)"},{"key":"10_CR37","doi-asserted-by":"crossref","unstructured":"Stevens, M.: A survey of chosen-prefix collision attacks. In: London Mathematical Society Lecture Note Series, Cambridge University Press, pp. 182\u2013220 (2021)","DOI":"10.1017\/9781108854207.009"},{"key":"10_CR38","doi-asserted-by":"crossref","unstructured":"Stevens, M., Lenstra, A., De\u00a0Weger, B.: Chosen-prefix collisions for MD5 and colliding x. 509 certificates for different identities. In: Advances in Cryptology-EUROCRYPT 2007: 26th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Barcelona, Spain, May 20-24, 2007. Proceedings 26, pp. 1\u201322. Springer (2007)","DOI":"10.1007\/978-3-540-72540-4_1"},{"key":"10_CR39","doi-asserted-by":"publisher","unstructured":"TeReSe: Term Rewriting Systems. Cambridge University Press (2003). https:\/\/doi.org\/10.1017\/S095679680400526X","DOI":"10.1017\/S095679680400526X"},{"key":"10_CR40","unstructured":"The Tamarin Team: The Tamarin-Prover Manual June 4 (2019). https:\/\/tamarin-prover.com\/manual\/master\/tex\/tamarin-manual.pdf"},{"key":"10_CR41","unstructured":"Turner, J.: The keyed-hash message authentication code (HMAC). FIPS PUB 198-1, National Institute of Standards and Technology (NIST) (2008)"},{"key":"10_CR42","unstructured":"Wilcox, Z.: Lessons from the history of attacks on secure hash functions (2017). https:\/\/electriccoin.co\/blog\/lessons-from-the-history-of-attacks-on-secure-hash-functions\/"},{"key":"10_CR43","doi-asserted-by":"publisher","unstructured":"Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Narendran, P.: Theories of homomorphic encryption, unification, and the finite variant property. In: Chitil, O., King, A., Danvy, O. (eds.) Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming, Kent, Canterbury, United Kingdom, September 8\u201310, 2014, pp. 123\u2013133. ACM (2014). https:\/\/doi.org\/10.1145\/2643135.2643154","DOI":"10.1145\/2643135.2643154"},{"key":"10_CR44","doi-asserted-by":"crossref","unstructured":"Ylonen, T., Lonvick, C.: The secure shell (SSH) transport layer protocol, Technical report (2006)","DOI":"10.17487\/rfc4253"}],"container-title":["Lecture Notes in Computer Science","Computer Security \u2013 ESORICS 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-07891-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T02:19:52Z","timestamp":1779848392000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-07891-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,17]]},"ISBN":["9783032078902","9783032078919"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-07891-9_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,17]]},"assertion":[{"value":"17 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESORICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Research in Computer Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toulouse","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 September 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esorics2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.esorics2025.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}