View article

We reveal instances of unsoundness, incompleteness, and redundancy in the cryptographic protocol analysis logic of Gong, Needham and Yahalom. Solutions are proposed for each of these problems. The logic is extended to formalize the use of an uncerti ed key in the Yahalom protocol, and our analysis of the protocol suggests the possibility of a redundancy in the protocol.