In security protocol analysis, it is important to learn general principles that limit the abilities of an attacker, and that can be applied repeatedly to a variety of protocols. We introduce the notion of an ideal--a set of messages closed under encryption and invariant under composition with arbitrary messages--to express such principles. In conjunction with the strand space formalism, we use the concept of ideals to prove bounds on a penetrator's capabilities, independent of the security protocol being analyzed. From this we prove a number of correctness properties of the Otway Rees protocol, using these results to explain the limitations of the protocol.
F. Javier Thayer, Jonathan C. Herzog, Joshua D. Gu