{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:23:54Z","timestamp":1725891834951},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540472377"},{"type":"electronic","value":"9783540472384"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901914_31","type":"book-chapter","created":{"date-parts":[[2006,10,10]],"date-time":"2006-10-10T05:21:43Z","timestamp":1160457703000},"page":"415-429","source":"Crossref","is-referenced-by-count":0,"title":["Monotonic Set-Extended Prefix Rewriting and Verification of Recursive Ping-Pong Protocols"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Esparza","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"4","key":"31_CR1","first-page":"267","volume":"5","author":"M. Abadi","year":"1998","unstructured":"Abadi, M., Gordon, A.D.: A bisimulation method for cryptographic protocols. Nordic Journal of Computing\u00a05(4), 267\u2013303 (1998)","journal-title":"Nordic Journal of Computing"},{"issue":"2","key":"31_CR2","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"P.A. Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation\u00a0127(2), 91\u2013101 (1996)","journal-title":"Information and Computation"},{"key":"31_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-45694-5_33","volume-title":"CONCUR 2002 - Concurrency Theory","author":"R.M. Amadio","year":"2002","unstructured":"Amadio, R.M., Charatonik, W.: On name generation and set-based analysis in the Dolev-Yao model. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 499\u2013514. Springer, Heidelberg (2002)"},{"issue":"1","key":"31_CR4","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1016\/S0304-3975(02)00090-7","volume":"290","author":"R.M. Amadio","year":"2002","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 (2002)","journal-title":"Theoretical Computer Science"},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"31_CR6","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF01969548","volume":"6","author":"J.R. B\u00fcchi","year":"1964","unstructured":"B\u00fcchi, J.R.: Regular canonical systems. Arch. Math. Logik u. Grundlagenforschung\u00a06, 91\u2013111 (1964)","journal-title":"Arch. Math. Logik u. Grundlagenforschung"},{"issue":"1","key":"31_CR7","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1006\/inco.1996.0003","volume":"124","author":"G. C\u00e9c\u00e9","year":"1996","unstructured":"C\u00e9c\u00e9, G., Finkel, A., Purushothaman Iyer, S.: Unreliable channels are easier to verify than perfect channels. Information and Computation\u00a0124(1), 20\u201331 (1996)","journal-title":"Information and Computation"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/3-540-48224-5_56","volume-title":"Automata, Languages and Programming","author":"H. Comon","year":"2001","unstructured":"Comon, H., Cortier, V., Mitchell, J.: Tree automata with one memory, set constraints, and ping-pong protocols. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol.\u00a02076, pp. 682\u2013693. Springer, Heidelberg (2001)"},{"issue":"1\u20133","key":"31_CR9","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0019-9958(82)90401-6","volume":"55","author":"D. Dolev","year":"1982","unstructured":"Dolev, D., Even, S., Karp, R.M.: On the security of ping-pong protocols. Information and Control\u00a055(1\u20133), 57\u201368 (1982)","journal-title":"Information and Control"},{"issue":"2","key":"31_CR10","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"IT-29","author":"D. Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. Transactions on Information Theory\u00a0IT-29(2), 198\u2013208 (1983)","journal-title":"Transactions on Information Theory"},{"key":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"31_CR12","unstructured":"H\u00fcttel, H., Srba, J.: Recursive ping-pong protocols. In: Proceedings of the 4th International Workshop on Issues in the Theory of Security (WITS 2004), pp. 129\u2013140 (2004)"},{"key":"31_CR13","series-title":"Lecture Notes in Computer Science","first-page":"175","volume-title":"SOFSEM 2005: Theory and Practice of Computer Science","author":"H. H\u00fcttel","year":"2005","unstructured":"H\u00fcttel, H., Srba, J.: Recursion vs. replication in simple cryptographic protocols. In: Vojt\u00e1\u0161, P., Bielikov\u00e1, M., Charron-Bost, B., S\u00fdkora, O. (eds.) SOFSEM 2005. LNCS, vol.\u00a03381, pp. 175\u2013184. Springer, Heidelberg (2005)"},{"issue":"3","key":"31_CR14","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1145\/377978.377993","volume":"2","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.: Weak alternating automata are not that weak. ACM Transactions on Computational Logic\u00a02(3), 408\u2013429 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"31_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/3-540-45694-5_34","volume-title":"CONCUR 2002 - Concurrency Theory","author":"R. K\u00fcsters","year":"2002","unstructured":"K\u00fcsters, R.: On the decidability of cryptographic protocols with open-ended data structures. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 515\u2013530. Springer, Heidelberg (2002)"},{"key":"31_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-28644-8_23","volume-title":"CONCUR 2004 - Concurrency Theory","author":"M. K\u0159et\u00ednsk\u00fd","year":"2004","unstructured":"K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: Extended process rewrite systems: Expressiveness and reachability. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 355\u2013370. Springer, Heidelberg (2004)"},{"key":"31_CR17","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1109\/LICS.1988.5139","volume-title":"Proceedings of the 3rd Annual IEEE Symposium on Logic in Computer Science (LICS 1988)","author":"D.E. Muller","year":"1988","unstructured":"Muller, D.E., Saoudi, A., Schupp, P.E.: Weak alternating automata give a simple explanation of why most temporal and dynamic logics are decidable in exponential time. In: Proceedings of the 3rd Annual IEEE Symposium on Logic in Computer Science (LICS 1988), pp. 422\u2013427. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"31_CR18","doi-asserted-by":"crossref","unstructured":"Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions and composed keys is NP-complete. TCS: Theoretical Computer Science\u00a0299 (2003)","DOI":"10.1016\/S0304-3975(02)00490-5"},{"key":"31_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2086.001.0001","volume-title":"Concurrent Constraint Programming","author":"V.A. Saraswat","year":"1993","unstructured":"Saraswat, V.A.: Concurrent Constraint Programming. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901914_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,2]],"date-time":"2021-08-02T00:18:10Z","timestamp":1627863490000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901914_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540472377","9783540472384"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11901914_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}