Proving security protocols has been a challenge ever since Needham and Schroeder threw down the gauntlet in their pioneering 1978 paper: Protocols such as those developed here are prone to extremely subtle errors that are unlikely to be detected in normal operation. The need for techniques to verify the correctness of such protocols is great, and we encourage those interested in such problems to consider this area. [12] This may not seem such a grand challenge, at first, as most cryptographic protocols can be written in half a dozen lines and involve even fewer players; the twist is the intruder, who actively interferes with proceedings: We assume that an intruder can interpose a computer on all communication paths, and thus can alter or copy parts of messages, replay messages, or emit false material. [12]