Deciding security for protocols with recursive tests

Deciding security for protocols with recursive tests. Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. In Proceedings of the 23rd International Conference on Automated Deduction (CADE'11), pp. 49–63, Lecture Notes in Artificial Intelligence, Springer, Wrocław, Poland, July 2011.

Download

[PDF] [HTML]

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.
While considering general recursive input\slashoutput 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.

BibTeX

@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},
}