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.