Decidable Analysis for a Class of Cryptographic Group Protocols with Unbounded Lists

Cryptographic protocols are crucial for securing electronic transactions. The confidence in these protocols can be increased by the formal analysis of their security properties. Although many works have been dedicated to standard protocols like Needham-Schroeder very few address the more challenging class of group protocols. We have introduced in previous work a synchronous model for group protocols, that generalizes standard protocol models by permitting unbounded lists inside messages. This approach also applies to analyzing Web services manipulating sequences of items. In this model we propose now a decision procedure for the sub-class of well-tagged protocols with autonomous keys.