Deciding security for protocols with recursive tests - Archive ouverte HAL Access content directly
Conference Papers Year : 2011

Deciding security for protocols with recursive tests

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.

Dates and versions

inria-00638557 , version 1 (05-11-2011)

Identifiers

Cite

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⟩
80 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More