Abstract
We investigate conditions under which an infinite set of atomic messages can be replaced with one or two values without affecting the correctness of a security protocol. The work is conducted using the strand spaces formalism, but the results apply to all protocol analysis techniques, and should be of particular value to those using model checking. The implications of the central result are discussed. Copyright 2006 ACM.