Skip to Main content Skip to Navigation
Conference papers

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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadatas
Contributor : Véronique Cortier <>
Submitted on : Saturday, November 5, 2011 - 9:39:56 PM
Last modification on : Friday, January 15, 2021 - 3:24:26 AM

Links full text



Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune. Deciding security for protocols with recursive tests. 23rd International Conference on Automated Deduction (CADE'11), Aug 2011, Wroclaw, Poland. pp.49-63, ⟨10.1007/978-3-642-22438-6_6⟩. ⟨inria-00638557⟩



Record views