Deciding security for protocols with recursive tests

Mathilde Arnaud Véronique Cortier 1 Stéphanie Delaune
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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\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.
Type de document :
Communication dans un congrès
Bj\orner, Nikolaj and Sofronie-Stokkermans, Viorica. 23rd International Conference on Automated Deduction (CADE'11), Aug 2011, Wroclaw, Poland. Springer, pp.49-63, 2011, 〈10.1007/978-3-642-22438-6_6〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00638557
Contributeur : Véronique Cortier <>
Soumis le : samedi 5 novembre 2011 - 21:39:56
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10

Identifiants

Citation

Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune. Deciding security for protocols with recursive tests. Bj\orner, Nikolaj and Sofronie-Stokkermans, Viorica. 23rd International Conference on Automated Deduction (CADE'11), Aug 2011, Wroclaw, Poland. Springer, pp.49-63, 2011, 〈10.1007/978-3-642-22438-6_6〉. 〈inria-00638557〉

Partager

Métriques

Consultations de la notice

234