Ping-pong protocols as prefix grammars: Modelling and verification via program transformation

• We model ping-pong protocols by prefix grammars.
• A criterion of vulnerability of a protocol model can be used by a supercompiler.
• Terminating unfolding up to the criterion allows to describe a set of attack models.
• Complexity of the verification process by unfolding is exponential.

This paper presents a technique to model ping-pong protocols by prefix grammars in such a way that the security of the protocol models becomes decidable by a general-purpose program transformation tool with unfolding. The presented approach not only decides whether a protocol model is insecure but also builds a set of possible attack models explicitly.