Paper Info
Title
Automata-Based Analysis of Recursive Cryptographic Protocols
Abstract
Cryptographic protocols can be divided into (1) protocols where the protocol steps are simple from a computational point of view and can thus be modeled by simple means, for instance, single rewrite rules-we call these protocols non-looping-and (2) protocols, such as group protocols, where the protocol steps are complex and typically involve an iterative or recursive computation-we call them recursive. While much is known on the decidability of security for non-looping protocols, only little is known for recursive protocols. In this paper, we prove decidability of security (w.r.t. the standard Dolev-Yao intruder) for a core class of recursive protocols and undecidability for several extensions. The key ingredient of our protocol model are specifically designed tree transducers which work over infinite signatures and have the ability to generate new constants (which allow us to mimic key generation). The decidability result is based on an automata-theoretic construction which involves a new notion of regularity, designed to work well with the infinite signatures we use.
Year
DOI
Venue
2004
10.1007/978-3-540-24749-4_34
Lecture Notes in Computer Science
Keywords
Field
DocType
cryptographic protocol
Key generation,Discrete mathematics,Combinatorics,Tree (graph theory),Cryptographic protocol,Computer science,Iterative method,Automaton,Decidability,Theoretical computer science,Tree automaton,Recursion
Conference
Volume
ISSN
Citations 
2996
0302-9743
16
PageRank 
References 
Authors
0.76
20
2
Name
Order
Citations
PageRank
Ralf Küsters1101469.62
Thomas Wilke21028.76