On the Decidability of Cryptographic Protocols with Open-ended Data Structures

Formal analysis of cryptographic protocols has mainly concentrated on protocols with closed-ended data structures. That is, the messages exchanged between principals have fixed and finite format. However, in many protocols the data structures used are open-ended, i.e., messages have an unbounded number of data fields. This work studies decidability issues for protocols with open-ended data structures. We propose a protocol model in which principals are described by transducers, i.e., finite automata with output, and show that in this model security -- in presence of the standard Dolev-Yao intruder -- is decidable and PSPACE-hard.

Logo BII

BII

Zitieren

Zitierform:
Zitierform konnte nicht geladen werden.

Rechte

Nutzung und Vervielfältigung:Keine Creative-Commons-Lizenz - Es gelten die Bestimmungen des dt. Urheberrechts (UrhG)Bitte beachten Sie, dass einzelne Bestandteile der Publikation anderweitigen Lizenz- bzw. urheberrechtlichen Bedingungen unterliegen können.