  Multi-protocol attacks due to protocol interaction has been a notorious
problem for security. Gutman-Thayer proved that they can be prevented by
ensuring that encrypted messages are distinguishable across protocols, under a
free algebra. In this paper, we prove that a similar suggestion prevents these
attacks under commonly used operators such as Exclusive-OR, that induce
equational theories, breaking the free algebra assumption.
