Deciding security for protocols with recursive tests. Research Report LSV-11-05, Laboratoire Spécification et Vérification

Abstract. Security protocols aim at securing communications over pub-lic networks. Their design is notoriously difficult and error-prone. Formal methods have shown their usefulness for providing a careful security anal-ysis in the case of standard authentication and confidentiality protocols. However, most current techniques do not apply to protocols that per-form 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 proto-cols, 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 attacker knowledge.