Many techniques for protocol analysis use term re placement rules to express the reduction properties of symbolic encryption operations. Some approaches must solve equations in those operators, using sequences of narrowing steps. It is shown that every infinite sequence of narrowing steps for popular abstract encryption operators has a loop, and hence there is a terminating algorithm to solve such equations by searching all sequences of narrowing steps.

• narr_term.ps