2011 | OriginalPaper | Buchkapitel
Deciding Security for Protocols with Recursive Tests
verfasst von : Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune
Erschienen in: Automated Deduction – CADE-23
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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 attacker knowledge.