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

New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols. Hubert Comon-Lundh and Véronique Cortier. In Proceedings of the 14th International Conference on Rewriting Techniques and Applications (RTA'03), pp. 148–164, Lecture Notes in Computer Science 2706, Springer, Valencia, Spain, June 2003.

Download

[PDF] [PS] [HTML]

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.

BibTeX

@inproceedings{rta03,
  address =       {Valencia, Spain},
  author =        {Comon{-}Lundh, Hubert and Cortier, V{\'e}ronique},
  booktitle =     {{P}roceedings of the 14th {I}nternational
                   {C}onference on {R}ewriting {T}echniques and
                   {A}pplications ({RTA}'03)},
  editor =        {Nieuwenhuis, Robert},
  month =         jun,
  pages =         {148-164},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {New Decidability Results for Fragments of First-Order
                   Logic and Application to Cryptographic Protocols},
  volume =        {2706},
  year =          {2003},
  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.},
  doi = {10.1007/3-540-44881-0_12},
}