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-Schroder very few address the more challenging class of group protocols. We have introduced in previous work [6] a synchronous model for group protocols, that generalizes standard protocol models by permitting unbounded lists inside messages. This approach also applies to analyze 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.

• Type: Conference
• Year: 2009
• Where: CSFW
• Authors: Najah Chridi, Mathieu Turuani, Michaël Rusinowitch
• Keywords: Cryptographic Protocols, CSFW 2009, Group Protocols, Security Privacy, Standard Protocol