Flat and one-variable clauses: Complexity of verifying cryptographic protocols with single blind copying

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.

REFERENCES

• 1: Alexander Aiken , Dexter Kozen , Moshe Y. Vardi , Edward L. Wimmers, The Complexity of Set Constraints, Selected Papers from the 7th Workshop on Computer Science Logic, p.1-17, September 13-17, 1993
• 2: Roberto M. Amadio , Witold Charatonik, On Name Generation and Set-Based Analysis in the Dolev-Yao Model, Proceedings of the 13th International Conference on Concurrency Theory, p.499-514, August 20-23, 2002
• 3: Roberto M. Amadio , Denis Lugiez, On the Reachability Problem in Cryptographic Protocols, Proceedings of the 11th International Conference on Concurrency Theory, p.380-394, August 22-25, 2000
• 4: 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.
• 5: 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.
• 6: Leo Bachmair , Harald Ganzinger , Uwe Waldmann, Superposition with Simplification as a Desision Procedure for the Monadic Class with Equality, Proceedings of the Third Kurt Gödel Colloquium on Computational Logic and Proof Theory, p.83-96, August 24-27, 1993
• 7: Bruno Blanchet, An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.82, June 11-13, 2001
• 8: Ashok K. Chandra , Dexter C. Kozen , Larry J. Stockmeyer, Alternation, Journal of the ACM (JACM), v.28 n.1, p.114-133, Jan. 1981 [doi>10.1145/322234.322243]
• 9: W. Charatonik , A. Podelski, Set constraints with intersection, Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, p.362, June 29-July 02, 1997
• 10: Hubert Comon , Véronique Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science, v.331 n.1, p.143-214, 15 February 2005 [doi>10.1016/j.tcs.2004.09.036]
• 11: Hubert Comon , Véronique Cortier , John Mitchell, Tree Automata with One Memory, Set Constraints, and Ping-Pong Protocols, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.682-693, July 08-12, 2001
• 12: 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.
• 13: 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.
• 14: Cortier, V. 2003. Vérification automatique des protocoles cryptographiques. Ph.D. dissertation. ENS Cachan, Cachan, France.
• 15: 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).
• 16: Fermüller, C., Leitsch, A., Hustadt, U., and Tammet, T. 2001. Resolution Decision Procedures, Chapter 25, 1791--1849. Volume II of Robinson and Voronkov {2001}.
• 17: Marcelo Fiore , Martín Abadi, Computing Symbolic Models for Verifying Cryptographic Protocols, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.160, June 11-13, 2001
• 18: Harald Ganzinger , Konstantin Korovin, New Directions in Instantiation-Based Theorem Proving, Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, p.55, June 22-25, 2003
• 19: Jean Goubault, Proving with BDDs and Control of Information, Proceedings of the 12th International Conference on Automated Deduction, p.499-513, June 26-July 01, 1994
• 20: Jean Goubault-Larrecq, A Method for Automatic Cryptographic Protocol Verification, Proceedings of the 15 IPDPS 2000 Workshops on Parallel and Distributed Processing, p.977-984, May 01-05, 2000
• 21: Jean Goubault-Larrecq, Higher-Order Positive Set Constraints, Proceedings of the 16th International Workshop and 11th Annual Conference of the EACSL on Computer Science Logic, p.473-489, September 22-25, 2002
• 22: Goubault-Larrecq, J. 2004. Résolution ordonnée avec sélection et classes décidables de la logique du premier ordre. Lecture notes for the course “démonstration automatique et vérification de protocoles cryptographiques” (with Hubert Comon-Lundh), DEA “programmation.” 71 pages. Available online at http://www.lsv.ens-cachan.fr/~goubault/SOresol.ps.
• 23: Goubault-Larrecq, J., Roger, M., and Verma, K. N. 2005. Abstraction and resolution modulo AC: How to verify Diffie-Hellman-like protocols automatically. J. Log. Algebr. Program. 64, 2 (Aug.), 219--251.
• 24: William H. Joiner, Jr., Resolution Strategies as Decision Procedures, Journal of the ACM (JACM), v.23 n.3, p.398-417, July 1976 [doi>10.1145/321958.321960]
• 25: Kleene, S. 2002. Mathematical Logic. Dover, New York, NY.
• 26: Lee, S.-J. and Plaisted, D. 1992. Eliminating duplication with the hyper-linking strategy. J. Automat. Reason. 9, 1, 25--42.
• 27: Alberto Martelli , Ugo Montanari, An Efficient Unification Algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.2, p.258-282, April 1982 [doi>10.1145/357162.357169]
• 28: Maslov, S. J. 1964. An inverse method of establishing deducibility in the classical predicate calculus. Sov. Math. Dokl. 5, 1420--1424.
• 29: David Monniaux, Abstracting Cryptographic Protocols with Tree Automata, Proceedings of the 6th International Symposium on Static Analysis, p.149-163, September 22-24, 1999
• 30: Flemming Nielson , Hanne Riis Nielson , Helmut Seidl, Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi, Proceedings of the 9th International Symposium on Static Analysis, p.20-35, September 17-20, 2002
• 31: 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.
• 32: Alan Robinson , Andrei Voronkov, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 33: Michaël Rusinowitch , Mathieu Turuani, Protocol Insecurity with Finite Number of Sessions is NP-Complete, Proceedings of the 14th IEEE workshop on Computer Security Foundations, p.174, June 11-13, 2001
• 34: Christoph Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, Proceedings of the 16th International Conference on Automated Deduction: Automated Deduction, p.314-328, July 07-10, 1999

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving
          Subjects: Resolution

General Terms:
Security, Theory, Verification

Keywords:
Cryptographic protocols, Horn clauses, first-order logic, instantiation-based theorem proving, resolution