On the Decidability of Cryptographic Group Protocols
We propose a protocol model in which principals are described by transducers (Mealy machines), i.e., finite automata with output. This allows the principals to process messages with an unbounded number of data fields, a requirement typical for group protocols. However, as in other models, a finite number of sessions and protocol steps is assumed. For this setting, we show security to be decidable provided that the nesting depth of encryptions and hashes performed by the intruder is bounded.