Many techniques for protocol analysis use term replacement 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.

A model is presented for the ring bracket mechanism, and its security properties, particularly in relation to the Bell and La Padula secrecy model and the Biba integrity model, are examined. It is found that if privilege, secrecy, and integrity are related to each other in a natural manner, then: (1) the ring bracket mechanism can be used to enforce either the Bell and La Padula secrecy policy or the Biba integrity policy, but not both in a nontrivial way; (2) the ring bracket mechanism for SCOMP, the Honeywell secure communications processor, cannot be used to enforce either policy in a reasonable way. The ring bracket mechanism for SCOMP satisfies a variant of the Biba integrity policy oriented toward program execution. A ring bracket mechanism similar to that of SCOMP can be reconstructed from a general ring bracket mechanism by requiring the following conditions: (1) program execution version of the Biba integrity policy; (2) reduction of redundancy between execute access mode and call access mode: and (3) consistent privilege.>