to infinity and beyond or, avoiding the infinite in security protocol analysis
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.
security protocols strand spaces model checking