Honest ideals on strand spaces

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. The authors 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, they use the concept of ideals to prove bounds on a penetrator´s capabilities, independent of the security protocol being analyzed. From this they prove a number of correctness properties of the Otway Rees protocol, using these results to explain the limitations of the protocol