Joel Alwen
New York University

On Formal Models for Secure Key Exchange


A new formal security model for session key exchange protocols is
proposed, and several efficient protocols are analysed in this model.
The new model is in the style of multi-party simulatability: it
specifies the service and security guarantees that a key exchange
protocol should provide to higher-level protocols as a simple, natural,
and intuitive interface to which a high-level protocol designer can
program. The relationship between this new model and previously proposed
models is explored, and in particular, several flaws and shortcomings in
previously proposed models are discussed. The model also deals with
anonymous users-that is, users who do not have public keys, but perhaps
have passwords that can be used to authenticate themselves within a
secure session.

As the allotted time for the seminar does not allow for a detailed
presentation of all aspects of this paper, we will mainly focus on the
description and intuition behind the model, the Diffie-Hellman based
protocols and the consequences of security against (strong) adaptive
corruption vs. against static corruption. Finally we will briefly
discuss the Bellare-Rogaway Model and comment on some of it's properties
and how it relates to the new approach.

Victor Shoup