Transducer-based analysis of cryptographic protocols

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, by 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 whi...

• Type: Journal
• Year: 2007
• Where: IANDC
• Authors: Ralf Küsters, Thomas Wilke
• Keywords: Cryptographic Protocols, IANDC 2007, Protocol Steps, Recursive Protocols