Deciding Security for Protocols with Recursive Tests

9 years 2 months ago
Deciding Security for Protocols with Recursive Tests
Abstract. Security protocols aim at securing communications over public networks. Their design is notoriously difficult and error-prone. Formal methods have shown their usefulness for providing a careful security analysis in the case of standard authentication and confidentiality 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/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 certification 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 atta...
Mathilde Arnaud, Véronique Cortier, St&eacu
Added 13 Dec 2011
Updated 13 Dec 2011
Type Journal
Year 2011
Where CADE
Authors Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune
Comments (0)