On Formal Models for Secure Key Exchange.

A new formal security model for session key exchange protocols in the public key setting is proposed, and several efficient protocols are analyzed in this model. The relationship between this new model and previously proposed models is explored, and several interesting, subtle distinctions between static and adaptive adversaries are explored. We also give a brief account of anonymous users. 1 Introduction In this paper, we investigate formal models of security for authenticated key exchange protocols in a public key setting where the only trusted party is an off-line certification authority. Our work follows up on that of Bellare, Canetti, and Krawczyk [2], which is grounded in the multi-party simulatability tradition (see, e.g., [1]). This approach seems very attractive, because it formulates security in terms of the service a session key protocol should provide to a higher level protocol, rather than getting mired in the details of session key protocols themselves, many of which ar...