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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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.
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.
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.
D. Bolignano. Towards the mechanization of cryptographic protocol verificatio. In 9th. Conf. on Computer Aided Verification, volume 1254 of LNCS, 1997.
L. Bozga, Y. Lakhnech, and M. Périn. Abstract interpretation for secrecy using patterns. In Proc. TACAS, LNCS, 2003. To appear.
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.
J. Clarkand J. Jacob. A survey of authentication protocol literature: Version, 1997.
E. Cohen. TAPS: A first-order verifier for cryptographic protocols. In 13th Computer Security Foundations Workshop (CSFW’00). IEEE Computer Society Press, 2000.
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.
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.
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.
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.
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.
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.
N. Dershowitz. Rewriting. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 1, chapter 9. North Holland, 2001.
N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In Proc. Workshop on formal methods in security protocols, 1999.
F. T. Fabrega, J. Herzog, and J. Guttman. Strand spaces: Proving security protocol correct. Journal of Computer Security, 7:191–230, 1999.
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.
J. Goubault-Larrecq and I. Mackie. Proof Theory and Automated Deduction, volume 6 of Applied Logic Series. Kluwer Academic, 1997.
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.
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.
D. McAllester. Automatic recognition of tractability in inference relations. J. ACM, 40(2):284–303, 1993.
P. Narendran, Q. Guo, and D. Wolfram. Unification and matching modulo nilpotence. In Proc. CADE-13, volume 1104 of LNCS, pages 261–274, 1996.
L. Paulson. Mechanized proofs for a recursive authentication protocol. In Proc. 10th IEEE Computer Security Foundations Workshop, pages 84–95, 1997.
L. C. Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 6(1):85–128, 1998.
M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In 14th IEEE Computer Security Foundations Workshop, 2001.
P. Ryan and S. Schneider. An attackon a recursive authentication protocol: A cautionary tale. Information Processing Letters, 65(1):7–10, 1998.
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.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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