{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,30]],"date-time":"2022-12-30T05:21:12Z","timestamp":1672377672664},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"4","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2008,8]]},"abstract":"Cryptographic protocols with single blind copying were defined and modeled by Comon and Cortier using the new class C of first-order clauses. They showed its satisfiability problem to be in 3-DEXPTIME. We improve this result by showing that satisfiability for this class is NEXPTIME-complete, using new resolution techniques. We show satisfiability to be DEXPTIME-complete if clauses are Horn, which is what is required for modeling cryptographic protocols. While translation to Horn clauses only gives a DEXPTIME upper bound for the secrecy problem for these protocols, we further show that this secrecy problem is actually DEXPTIME-complete.<\/jats:p>","DOI":"10.1145\/1380572.1380577","type":"journal-article","created":{"date-parts":[[2008,9,4]],"date-time":"2008-09-04T12:51:35Z","timestamp":1220532695000},"page":"1-45","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Flat and one-variable clauses"],"prefix":"10.1145","volume":"9","author":[{"given":"Helmut","family":"Seidl","sequence":"first","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Garching, Germany"}]},{"given":"Kumar Neeraj","family":"Verma","sequence":"additional","affiliation":[{"name":"Technische Universit\u00e4t M\u00fcnchen, Garching, Germany"}]}],"member":"320","published-online":{"date-parts":[[2008,8,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of CSL'93","volume":"832","author":"Aiken A.","unstructured":"Aiken , A. , Kozen , D. , Vardi , M. , and Wimmers , E . 1993. The complexity of set constraints . In Proceedings of CSL'93 . Lecture Notes in Computer Science , vol. 832 . Springer-Verlag, Berlin, Germany, 1--17. Aiken, A., Kozen, D., Vardi, M., and Wimmers, E. 1993. The complexity of set constraints. In Proceedings of CSL'93. Lecture Notes in Computer Science, vol. 832. Springer-Verlag, Berlin, Germany, 1--17."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the 13th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science","volume":"2421","author":"Amadio R.","unstructured":"Amadio , R. and Charatonik , W . 2002. On name generation and set-based analysis in the Dolev-Yao model . In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science , vol. 2421 , Springer-Verlag, Berlin, Germany, 499--514. Amadio, R. and Charatonik, W. 2002. On name generation and set-based analysis in the Dolev-Yao model. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 2421, Springer-Verlag, Berlin, Germany, 499--514."},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the 11th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science","volume":"1877","author":"Amadio R.","unstructured":"Amadio , R. and Lugiez , D . 2000. On the reachability problem in cryptographic protocols . In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science , vol. 1877 , Springer-Verlag, Berlin, Germany, 380--394. Amadio, R. and Lugiez, D. 2000. On the reachability problem in cryptographic protocols. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR). Lecture Notes in Computer Science, vol. 1877, Springer-Verlag, Berlin, Germany, 380--394."},{"key":"e_1_2_1_4_1","first-page":"19","article-title":"Resolution theorem proving. In Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov, Eds. Vol. I. North-Holland, Amsterdam, The Netherlands","volume":"2","author":"Bachmair L.","year":"2001","unstructured":"Bachmair , L. and Ganzinger , H. 2001 . Resolution theorem proving. In Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov, Eds. Vol. I. North-Holland, Amsterdam, The Netherlands , Chapter 2 , 19 -- 99 . Bachmair, L. and Ganzinger, H. 2001. Resolution theorem proving. In Handbook of Automated Reasoning, J. A. Robinson and A. Voronkov, Eds. Vol. I. North-Holland, Amsterdam, The Netherlands, Chapter 2, 19--99.","journal-title":"Chapter"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press","author":"Bachmair L.","unstructured":"Bachmair , L. , Ganzinger , H. , and Waldmann , U . 1993a. Set constraints are the monadic class . In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press , Los Alamitos, CA, 75--83. Bachmair, L., Ganzinger, H., and Waldmann, U. 1993a. Set constraints are the monadic class. In Proceedings of the 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 75--83."},{"key":"e_1_2_1_6_1","volume-title":"3rd Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory. Lecture Notes in Computer Science","volume":"713","author":"Bachmair L.","unstructured":"Bachmair , L. , Ganzinger , H. , and Waldmann , U . 1993b. Superposition with simplification as a desision procedure for the monadic class with equality . In 3rd Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory. Lecture Notes in Computer Science , vol. 713 . Springer-Verlag, Berlin, Germany, 83--96. Bachmair, L., Ganzinger, H., and Waldmann, U. 1993b. Superposition with simplification as a desision procedure for the monadic class with equality. In 3rd Kurt G\u00f6del Colloquium on Computational Logic and Proof Theory. Lecture Notes in Computer Science, vol. 713. Springer-Verlag, Berlin, Germany, 83--96."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.5555\/872752.873511"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97)","author":"Charatonik W.","unstructured":"Charatonik , W. and Podelski , A . 1997. Set constraints with intersection . In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97) . IEEE Computer Society Press, Los Alamitos, CA, 362--372. Charatonik, W. and Podelski, A. 1997. Set constraints with intersection. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science (LICS'97). IEEE Computer Society Press, Los Alamitos, CA, 362--372."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.09.036"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of the 28th International Colloquium on Automata, Languages, and Programming (ICALP'2001)","volume":"2076","author":"Comon H.","unstructured":"Comon , H. , Cortier , V. , and Mitchell , J . 2001. Tree automata with one memory, set constraints and ping-pong protocols . In Proceedings of the 28th International Colloquium on Automata, Languages, and Programming (ICALP'2001) , F. Orejas, P. G. Spirakis, and J. van Leeuwen, Eds. Lecture Notes in Computer Science , vol. 2076 . Springer-Verlag, Berlin, Germany, 682--693. Comon, H., Cortier, V., and Mitchell, J. 2001. Tree automata with one memory, set constraints and ping-pong protocols. In Proceedings of the 28th International Colloquium on Automata, Languages, and Programming (ICALP'2001), F. Orejas, P. G. Spirakis, and J. van Leeuwen, Eds. Lecture Notes in Computer Science, vol. 2076. Springer-Verlag, Berlin, Germany, 682--693."},{"key":"e_1_2_1_12_1","volume-title":"Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03)","volume":"2706","author":"Comon-Lundh H.","unstructured":"Comon-Lundh , H. and Cortier , V . 2003a. New decidability results for fragments of first-order logic and application to cryptographic protocols . In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03) , R. Nieuwenhuis, Ed. Lecture Notes in Computer Science , vol. 2706 . Springer-Verlag, Berlin, Germany, 148--164. Comon-Lundh, H. and Cortier, V. 2003a. New decidability results for fragments of first-order logic and application to cryptographic protocols. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03), R. Nieuwenhuis, Ed. Lecture Notes in Computer Science, vol. 2706. Springer-Verlag, Berlin, Germany, 148--164."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 12th European Symposium on Programming (ESOP'03)","volume":"2618","author":"Comon-Lundh H.","unstructured":"Comon-Lundh , H. and Cortier , V . 2003b. Security properties: Two agents are sufficient . In Proceedings of the 12th European Symposium on Programming (ESOP'03) . Lecture Notes in Computer Science , vol. 2618 . Springer-Verlag, Berlin, Germany, 99--113. Comon-Lundh, H. and Cortier, V. 2003b. Security properties: Two agents are sufficient. In Proceedings of the 12th European Symposium on Programming (ESOP'03). Lecture Notes in Computer Science, vol. 2618. Springer-Verlag, Berlin, Germany, 99--113."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Workshop on Formal Methods and Security Protocols","author":"Durgin N. A.","unstructured":"Durgin , N. A. , Lincoln , P. , Mitchell , J. , and Scedrov , A . 1999. Undecidability of bounded security protocols . In Proceedings of the Workshop on Formal Methods and Security Protocols ( Trento, Italy). Durgin, N. A., Lincoln, P., Mitchell, J., and Scedrov, A. 1999. Undecidability of bounded security protocols. In Proceedings of the Workshop on Formal Methods and Security Protocols (Trento, Italy)."},{"key":"e_1_2_1_16_1","first-page":"1791","article-title":"Resolution Decision Procedures","volume":"25","author":"Ferm\u00fcller C.","year":"2001","unstructured":"Ferm\u00fcller , C. , Leitsch , A. , Hustadt , U. , and Tammet , T. 2001 . Resolution Decision Procedures , Chapter 25 , 1791 -- 1849 . Volume II of Robinson and Voronkov {2001}. Ferm\u00fcller, C., Leitsch, A., Hustadt, U., and Tammet, T. 2001. Resolution Decision Procedures, Chapter 25, 1791--1849. Volume II of Robinson and Voronkov {2001}.","journal-title":"Chapter"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01)","author":"Fiore M. P.","unstructured":"Fiore , M. P. and Abadi , M . 2001. Computing symbolic models for verifying cryptographic protocols . In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01) , P. Pandya and J. Radhakrishnan, Eds. IEEE Computer Society Press, Los Alamitos, CA, 160--173. Fiore, M. P. and Abadi, M. 2001. Computing symbolic models for verifying cryptographic protocols. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01), P. Pandya and J. Radhakrishnan, Eds. IEEE Computer Society Press, Los Alamitos, CA, 160--173."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03)","author":"Ganzinger H.","unstructured":"Ganzinger , H. and Korovin , K . 2003. New directions in instantiation-based theorem proving . In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03) , P. G. Kolaitis, Ed. IEEE Computer Society Press, Los Alamitos, CA, 55--64. Ganzinger, H. and Korovin, K. 2003. New directions in instantiation-based theorem proving. In Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), P. G. Kolaitis, Ed. IEEE Computer Society Press, Los Alamitos, CA, 55--64."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/648231.752981"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/645612.663136"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737422"},{"key":"e_1_2_1_22_1","volume-title":"\u201cd\u00e9monstration automatique et v\u00e9rification de protocoles cryptographiques","author":"Goubault-Larrecq J.","unstructured":"Goubault-Larrecq , J. 2004. R\u00e9solution ordonn\u00e9e avec s\u00e9lection et classes d\u00e9cidables de la logique du premier ordre. Lecture notes for the course \u201cd\u00e9monstration automatique et v\u00e9rification de protocoles cryptographiques \u201d (with Hubert Comon-Lundh) , DEA \u201cprogrammation.\u201d 71 pages. Available online at http:\/\/www.lsv.ens-cachan.fr\/~goubault\/SOresol.ps. Goubault-Larrecq, J. 2004. R\u00e9solution ordonn\u00e9e avec s\u00e9lection et classes d\u00e9cidables de la logique du premier ordre. Lecture notes for the course \u201cd\u00e9monstration automatique et v\u00e9rification de protocoles cryptographiques\u201d (with Hubert Comon-Lundh), DEA \u201cprogrammation.\u201d 71 pages. Available online at http:\/\/www.lsv.ens-cachan.fr\/~goubault\/SOresol.ps."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.09.004"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/321958.321960"},{"key":"e_1_2_1_25_1","volume-title":"Mathematical Logic","author":"Kleene S.","unstructured":"Kleene , S. 2002. Mathematical Logic . Dover , New York, NY . Kleene, S. 2002. Mathematical Logic. Dover, New York, NY."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00247825"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/357162.357169"},{"key":"e_1_2_1_28_1","first-page":"1420","article-title":"An inverse method of establishing deducibility in the classical predicate calculus","volume":"5","author":"Maslov S. J.","year":"1964","unstructured":"Maslov , S. J. 1964 . An inverse method of establishing deducibility in the classical predicate calculus . Sov. Math. Dokl. 5 , 1420 -- 1424 . Maslov, S. J. 1964. An inverse method of establishing deducibility in the classical predicate calculus. Sov. Math. Dokl. 5, 1420--1424.","journal-title":"Sov. Math. Dokl."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/647168.757020"},{"key":"e_1_2_1_30_1","volume-title":"Proceedings of the 9th Static Analysis Symposium (SAS'02)","volume":"24477","author":"Nielson F.","unstructured":"Nielson , F. , Nielson , H. R. , and Seidl , H . 2002. Normalizable Horn clauses, strongly recognizable relations and Spi . In Proceedings of the 9th Static Analysis Symposium (SAS'02) . Lecture Notes in Computer Science , vol. 24477 , Springer-Verlag, Berlin, Germany, 20--35. Nielson, F., Nielson, H. R., and Seidl, H. 2002. Normalizable Horn clauses, strongly recognizable relations and Spi. In Proceedings of the 9th Static Analysis Symposium (SAS'02). Lecture Notes in Computer Science, vol. 24477, Springer-Verlag, Berlin, Germany, 20--35."},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI'01)","author":"Riazanov A.","unstructured":"Riazanov , A. and Voronkov , A . 2001. Splitting without backtracking . In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI'01) . Morgan Kaufmann, San Francisco, CA, 611--617. Riazanov, A. and Voronkov, A. 2001. Splitting without backtracking. In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI'01). Morgan Kaufmann, San Francisco, CA, 611--617."},{"key":"e_1_2_1_32_1","volume-title":"Eds","author":"Robinson J. A.","year":"2001","unstructured":"Robinson , J. A. and Voronkov , A. , Eds . 2001 . Handbook of Automated Reasoning. North-Holland, Amsterdam, The Netherlands . Robinson, J. A. and Voronkov, A., Eds. 2001. Handbook of Automated Reasoning. North-Holland, Amsterdam, The Netherlands."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01)","author":"Rusinowitch M.","unstructured":"Rusinowitch , M. and Turuani , M . 2001. Protocol insecurity with finite number of sessions is NP-complete . In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01) , P. Pandya and J. Radhakrishnan, Eds. IEEE Computer Society Press, Los Alamitos, CA. Rusinowitch, M. and Turuani, M. 2001. Protocol insecurity with finite number of sessions is NP-complete. In Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW'01), P. Pandya and J. Radhakrishnan, Eds. IEEE Computer Society Press, Los Alamitos, CA."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753480"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1380572.1380577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T06:29:40Z","timestamp":1672295380000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1380572.1380577"}},"subtitle":["Complexity of verifying cryptographic protocols with single blind copying"],"short-title":[],"issued":{"date-parts":[[2008,8]]},"references-count":33,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2008,8]]}},"alternative-id":["10.1145\/1380572.1380577"],"URL":"http:\/\/dx.doi.org\/10.1145\/1380572.1380577","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,8]]},"assertion":[{"value":"2005-11-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2006-09-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-08-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}