Transducer-based analysis of cryptographic protocols

10 years 1 months ago
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...
Ralf Küsters, Thomas Wilke
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Authors Ralf Küsters, Thomas Wilke
Comments (0)