Analysis of Yahalom-Paulson Protocol in Strand Spaces

Based on strand spaces, this paper formally analyzes an important authentication protocol- the Yahalom-Paulson protocol from the aspects of both secrecy and authentication. The result shows that the session key distributed by the server is secure, but there is a flaw in the protocol, even if the responder and initiator receive keys, they may receive different keys. And then an improvement to this protocol is presented in order to enhance the security of the protocol.