Skip to main content
SpringerLink
Log in

New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols

  • Conference paper
  • First Online:
Book cover Rewriting Techniques and Applications (RTA 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2706))

Included in the following conference series:

Abstract

We consider a new extension of the Skolem class for first-order logic and prove its decidability by resolution techniques. We then extend this class including the built-in equational theory of exclusive or. Again, we prove the decidability of the class by resolution techniques. Considering such fragments of first-order logic is motivated by the automatic verification of cryptographic protocols, for an arbitrary number of sessions; the first-order formalization is an approximation of the set of possible traces, for instance relaxing the nonce freshness assumption. As a consequence, we get some new decidability results for the verification of cryptographic protocols with exclusive or.

Partially supported by INRIA project SECSI and RNTL project EVA.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Amadio and W. Charatonik. On name generation and set-based analysis in the dolev-yao model. In Proc. CONCUR 02, volume 1877 of LNCS, pages 380–394. Springer-Verlag, 2002.

    Google Scholar 

  2. L. Bachmair and H. Ganzinger. Resolution theorem proving. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, chapter 2, pages 19–100. North Holland, 2001.

    Google Scholar 

  3. B. Blanchet. Abstracting Cryptographic Protocols by Prolog Rules (invited +talk). In P. Cousot, editor, 8th International Static Analysis Symposium (SAS’2001), volume 2126 of LNCS, pages 433–436, Paris, France, July 2001. Springer Verlag.

    Google Scholar 

  4. D. Bolignano. Towards the mechanization of cryptographic protocol verificatio. In 9th. Conf. on Computer Aided Verification, volume 1254 of LNCS, 1997.

    Google Scholar 

  5. L. Bozga, Y. Lakhnech, and M. Périn. Abstract interpretation for secrecy using patterns. In Proc. TACAS, LNCS, 2003. To appear.

    Google Scholar 

  6. Y. Chevalier, R. Kuester, M. Rusinowitch, and M. Turuani. An np decision procedure for protocol insecurity with xor. In IEEE Logic in Comp. Science, to appear, 2003.

    Google Scholar 

  7. J. Clarkand J. Jacob. A survey of authentication protocol literature: Version, 1997.

    Google Scholar 

  8. E. Cohen. TAPS: A first-order verifier for cryptographic protocols. In 13th Computer Security Foundations Workshop (CSFW’00). IEEE Computer Society Press, 2000.

    Google Scholar 

  9. H. Comon and V. Cortier. Tree automata with one memory, set constraints and cryptographic protocols. Technical Report LSV-01-13, LSV, 2001. To appear in TCS.

    Google Scholar 

  10. H. Comon, V. Cortier, and J. Mitchell. Tree automata with memory, set constraints and ping pong protocols. In Proc. ICALP 2001, volume 2076 of LNCS. Springer Verlag, July 2001.

    Google Scholar 

  11. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. Available on: http://www.grappa.univ-lille3.fr/tata, 2002.

  12. H. Comon-Lundh and V. Cortier. New decidability results for fragments of first-order logic and application to cryptographic protocols. Technical Report LSV-03-3, LSV, ENS de Cachan, Cachan, France, January 2003. 30 pages.

    Google Scholar 

  13. H. Comon-Lundh and V. Cortier. Security properties: two agents are sufficient. In Proc. European Symposium on Programming, volume 2618 of LNCS, pages 99–113. Springer Verlag, 2003.

    Google Scholar 

  14. H. Comon-Lundh and V. Shmatikov. Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In Proc. IEEE Logic in Comp. Science, to appear, 2003.

    Google Scholar 

  15. N. Dershowitz. Rewriting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, chapter 9. North Holland, 2001.

    Google Scholar 

  16. N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. Workshop on formal methods in security protocols, 1999.

    Google Scholar 

  17. F. T. Fabrega, J. Herzog, and J. Guttman. Strand spaces: Proving security protocol correct. Journal of Computer Security, 7:191–230, 1999.

    Google Scholar 

  18. C. Fermuller, A. Leitsch, U. Hustadt, and T. Tamet. Resolution decision procedure. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 25, pages 1793–1849. North Holland, 2001.

    Google Scholar 

  19. J. Goubault-Larrecq and I. Mackie. Proof Theory and Automated Deduction, volume 6 of Applied Logic Series. Kluwer Academic, 1997.

    Google Scholar 

  20. R. Kowalski and P. Hayes. Semantic trees in automated theorem proving. In B. Meltzer and D. Michie, editors, Machine Intelligence 4, pages 87–101. Edinburgh University Press, 1969.

    Google Scholar 

  21. G. Lowe. Breaking and fixing the needham-schroeder public-key protocol using fdr. In Margaria and Steffen, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1055 of LNCS, pages 147–166, 1996.

    Google Scholar 

  22. D. McAllester. Automatic recognition of tractability in inference relations. J. ACM, 40(2):284–303, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  23. P. Narendran, Q. Guo, and D. Wolfram. Unification and matching modulo nilpotence. In Proc. CADE-13, volume 1104 of LNCS, pages 261–274, 1996.

    Google Scholar 

  24. L. Paulson. Mechanized proofs for a recursive authentication protocol. In Proc. 10th IEEE Computer Security Foundations Workshop, pages 84–95, 1997.

    Google Scholar 

  25. L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 6(1):85–128, 1998.

    Google Scholar 

  26. M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In 14th IEEE Computer Security Foundations Workshop, 2001.

    Google Scholar 

  27. P. Ryan and S. Schneider. An attackon a recursive authentication protocol: A cautionary tale. Information Processing Letters, 65(1):7–10, 1998.

    Article  Google Scholar 

  28. C. Weidenbach. Towards an automatic analysis of security protocols in first-order logic. In H. Ganzinger, editor, Proc. 16th Conference on Automated Deduction, volume 1632 of LNCS, pages 314–328, 1999.

    Chapter  Google Scholar 

  29. C. Weidenbach. Combining superposition, sorts and splitting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 27. North Holland, 2001.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire Spécification et Véreification, CNRS, Ecole Normale Supérieure de Cachan, France

    Hubert Comon-Lundh & Véronique Cortier

Authors
  1. Hubert Comon-Lundh
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Véronique Cortier
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dpt. Lenguajes y Sistemas Informáticos (LSI), Technical University of Catalonia (UPC), Jordi Girona 1, 08034, Barcelona, Spain

    Robert Nieuwenhuis

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Comon-Lundh, H., Cortier, V. (2003). New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols. In: Nieuwenhuis, R. (eds) Rewriting Techniques and Applications. RTA 2003. Lecture Notes in Computer Science, vol 2706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44881-0_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-44881-0_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40254-1

  • Online ISBN: 978-3-540-44881-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation