@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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},
}