{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,25]],"date-time":"2026-03-25T02:36:01Z","timestamp":1774406161064,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319118505","type":"print"},{"value":"9783319118512","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11851-2_11","type":"book-chapter","created":{"date-parts":[[2014,9,6]],"date-time":"2014-09-06T10:55:22Z","timestamp":1410000922000},"page":"162-177","source":"Crossref","is-referenced-by-count":23,"title":["A Formal Definition of Protocol Indistinguishability and Its Verification Using Maude-NPA"],"prefix":"10.1007","author":[{"given":"Sonia","family":"Santiago","sequence":"first","affiliation":[]},{"given":"Santiago","family":"Escobar","sequence":"additional","affiliation":[]},{"given":"Catherine","family":"Meadows","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Meseguer","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: POPL, pp. 104\u2013115 (2001)","DOI":"10.1145\/373243.360213"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Arapinis, M., Bursuc, S., Ryan, M.D.: Reduction of equational theories for verification of trace equivalence: Re-encryption, associativity and commutativity. In: Degano, P., Guttman, J.D. (eds.) POST 2012. LNCS, vol.\u00a07215, pp. 169\u2013188. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28641-4_10"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Barthe, G.B., Crespo, J.M., Gr\u00e9goire, B., Kunz, C., Lakhnech, Y., Schmidt, B., B\u00e9guelin, S.Z.: Fully automated analysis of padding-based encryption in the computational model. In: ACM Conference on Computer and Communications Security, pp. 1247\u20131260 (2013)","DOI":"10.1145\/2508859.2516663"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. ACM CCS 2005, pp. 16\u201325. ACM (2005)","DOI":"10.1145\/1102120.1102125"},{"key":"11_CR5","unstructured":"Bellovin, S., Merritt, M.: Encrypted key exchange: Password-based protocols secure against dictionary attacks. In: Proceedings of the 1992 Symposium on Research in Security and Privacy, pp. 72\u201384. IEEE (1992)"},{"issue":"1","key":"11_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.jlap.2007.06.002","volume":"75","author":"B. Blanchet","year":"2008","unstructured":"Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program.\u00a075(1), 3\u201351 (2008)","journal-title":"J. Log. Algebr. Program."},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Chadha, R., Ciob\u00e2c\u0103, \u015e., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol.\u00a07211, pp. 108\u2013127. Springer, Heidelberg (2012)","DOI":"10.1007\/978-3-642-28869-2_6"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-14203-1_35","volume-title":"Automated Reasoning","author":"V. Cheval","year":"2010","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Automating security analysis: symbolic equivalence of constraint systems. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 412\u2013426. Springer, Heidelberg (2010)"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: negative tests and non-determinism. In: Proc. ACM CCS 2011, pp. 321\u2013330 (2011)","DOI":"10.1145\/2046707.2046744"},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1007\/978-3-642-39799-8_50","volume-title":"Computer Aided Verification","author":"V. Cheval","year":"2013","unstructured":"Cheval, V., Cortier, V., Plet, A.: Lengths may break privacy \u2013 or how to check for equivalences with length. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 708\u2013723. Springer, Heidelberg (2013)"},{"issue":"6","key":"11_CR11","doi-asserted-by":"crossref","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"M. Clarkson","year":"2010","unstructured":"Clarkson, M., Schneider, F.: Hyperproperties. J. Computer Security\u00a018(6), 1157\u20131210 (2010)","journal-title":"J. Computer Security"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Cortier, V., Delaune, S.: A method for proving observational equivalence. In: CSF, pp. 266\u2013276. IEEE Computer Society (2009)","DOI":"10.1109\/CSF.2009.9"},{"key":"11_CR13","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 2007\/2008\/2009. LNCS, vol.\u00a05705, pp. 1\u201350. Springer, Heidelberg (2009)","DOI":"10.1007\/978-3-642-03829-7_1"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"Escobar, S., Meadows, C., Meseguer, J., Santiago, S.: A rewriting-based forwards semantics for Maude-NPA. In: Proc. HotSoS (to appear, 2014), Preliminary version available at: \n                  \n                    http:\/\/www.dsic.upv.es\/~sescobar\/papers\/HotSoS2014.pdf","DOI":"10.1145\/2600176.2600186"},{"issue":"7-8","key":"11_CR15","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.\u00a081(7-8), 898\u2013928 (2012)","journal-title":"J. Log. Algebr. Program."},{"key":"11_CR16","doi-asserted-by":"crossref","first-page":"191","DOI":"10.3233\/JCS-1999-72-304","volume":"7","author":"F.J. Thayer Fabrega","year":"1999","unstructured":"Thayer Fabrega, F.J., Herzog, J., Guttman, J.: Strand Spaces: What Makes a Security Protocol Correct? Journal of Computer Security\u00a07, 191\u2013230 (1999)","journal-title":"Journal of Computer Security"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-642-34005-5_9","volume-title":"Rewriting Logic and Its Applications","author":"R. Guti\u00e9rrez","year":"2012","unstructured":"Guti\u00e9rrez, R., Meseguer, J., Rocha, C.: Order-sorted equality enrichments modulo axioms. In: Dur\u00e1n, F. (ed.) WRLA 2012. LNCS, vol.\u00a07571, pp. 162\u2013181. Springer, Heidelberg (2012)"},{"issue":"1","key":"11_CR18","doi-asserted-by":"crossref","first-page":"83","DOI":"10.3233\/JCS-2004-12104","volume":"12","author":"G. Lowe","year":"2004","unstructured":"Lowe, G.: Analysings protocol subject to guessing attacks. Journal of Computer Security\u00a012(1), 83\u201398 (2004)","journal-title":"Journal of Computer Security"},{"key":"11_CR19","unstructured":"Merritt, M.: Cryptographic Protocols. PhD thesis, Georgia Inst. of Technology (1984)"},{"issue":"1","key":"11_CR20","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 united model of concurrency. Theor. Comput. Sci.\u00a096(1), 73\u2013155 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1007\/3-540-64299-4_26","volume-title":"Recent Trends in Algebraic Development Techniques","author":"J. Meseguer","year":"1998","unstructured":"Meseguer, J.: Membership algebra as a logical framework for equational specification. In: Parisi-Presicce, F. (ed.) WADT 1997. LNCS, vol.\u00a01376, pp. 18\u201361. Springer, Heidelberg (1998)"},{"key":"11_CR22","unstructured":"Newcomb, T., Lowe, G.: A computational justification for guessing attack formalisms. Technical report No. RR-05-05. Oxford University Computing Laboratory (October 2005)"},{"key":"11_CR23","unstructured":"TeReSe (ed.): Term Rewriting Systems. Cambridge Univ. Press, Cambridge (2003)"}],"container-title":["Lecture Notes in Computer Science","Security and Trust Management"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11851-2_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T19:55:36Z","timestamp":1558986936000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11851-2_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319118505","9783319118512"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11851-2_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014]]}}}