@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{ACD-cade11,
  address =       {Wroc{\l}aw, Poland},
  author =        {Arnaud, Mathilde and Cortier, V{\'e}ronique and
                   Delaune, St{\'e}phanie},
  booktitle =     {{P}roceedings of the 23rd {I}nternational
                   {C}onference on {A}utomated {D}eduction ({CADE}'11)},
  editor =        {Bj{\o}rner, Nikolaj and
                   Sofronie-Stokkermans, Viorica},
  month =         jul,
  pages =         {49-63},
  publisher =     {Springer},
  series =        {Lecture Notes in Artificial Intelligence},
  title =         {Deciding security for protocols with recursive tests},
  year =          {2011},
  abstract =      {Security protocols aim at securing communications
                   over public networks. Their design is notoriously
                   dicult and error-prone. Formal methods have shown
                   their usefulness for providing a careful security
                   analysis in the case of standard authentication and
                   condentiality protocols. However, most current
                   techniques do not apply to protocols that perform
                   recursive computation e.g. on a list of messages
                   received from the network.\par While considering
                   general recursive input{\slash}output actions very
                   quickly yields undecidability, we focus on protocols
                   that perform recursive tests on received messages but
                   output messages that depend on the inputs in a
                   standard way. This is in particular the case of
                   secured routing protocols, distributed right
                   delegation or PKI certication paths. We provide
                   NPTIME decision procedures for protocols with
                   recursive tests and for a bounded number of sessions.
                   We also revisit constraint system solving, providing
                   a complete symbolic representation of the attacker
                   knowledge.},
  doi =           {10.1007/978-3-642-22438-6_6},
}