Mathilde Arnaud, Véronique Cortier, and Stéphanie Delaune. Deciding security for protocols with recursive tests. 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.
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.
@inproceedings{ACD-cade11,
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.},
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)},
OPTDOI = {10.1007/978-3-642-22438-6_6},
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},
acronym = {{CADE}'11},
nmonth = {7},
OPTLONGPDF = {https://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/
rr-lsv-2011-05.pdf},
lsv-category = {intc},
wwwpublic = {public and ccsb},
}