A decidable subclass of unbounded security protocols
R. Ramanujam, S. P. Suresh · 2007
this paper, we propose a simple syntactic restriction on protocols and show that it achieves this purpose. The condition essentially states that between any two terms that occur in distinct communications, no encrypted subterm of one can be uni ed with a subterm of the other. In the absence of such a restriction, the intruder may use such a binding to transfer information from one play to another, and `pump' this process (using unboundedly many nonces) to generate unboundedly many plays with distinct information content, leading to undecidability. We show how the restriction leads to a bound on the size of (partial) runs that need to be checked for a leak. It is also easily seen that the subclass includes a wide variety of protocols studied in the literature, for instance, most of the protocols presented in the survey ([CJ97])