This paper presents a model and definitions for authenticated key exchange (AKE) protocols that are secure against dictionary attacks. The authors define a model that captures various security goals, including password guessing, forward secrecy, server compromise, and loss of session keys. They focus on AKE with implicit authentication, which is considered more fundamental than mutual authentication. The model is used to define the execution of authentication and key-exchange protocols in various settings, and provides a formal framework for analyzing the security of these protocols. The authors prove the security of the Encrypted Key-Exchange (EKE) protocol of Bellovin and Merritt in the ideal-cipher model. They define EKE2, which is a secure AKE protocol that provides forward secrecy. The protocol uses a Diffie-Hellman key exchange, where each flow is encrypted using the password. The shared session key is derived from a hash of the client and server identities and the exchanged values. The protocol also defines session IDs and partner IDs to ensure proper partnering and session freshness. The paper also discusses the addition of authentication to AKE protocols. It presents transformations that can be applied to an AKE protocol to provide client-to-server authentication, server-to-client authentication, or mutual authentication. These transformations use the distributed session key to construct an authenticator for the other party. The authors show that these transformations preserve the security properties of the original AKE protocol. The paper concludes with a discussion of ongoing work, including the analysis of EKE2 in the ideal-cipher model and the investigation of its security when the encryption function is instantiated with a random oracle. The authors also highlight the importance of considering the password space size in the context of dictionary attacks and the need for a robust model to capture the security requirements of password-based protocols.This paper presents a model and definitions for authenticated key exchange (AKE) protocols that are secure against dictionary attacks. The authors define a model that captures various security goals, including password guessing, forward secrecy, server compromise, and loss of session keys. They focus on AKE with implicit authentication, which is considered more fundamental than mutual authentication. The model is used to define the execution of authentication and key-exchange protocols in various settings, and provides a formal framework for analyzing the security of these protocols. The authors prove the security of the Encrypted Key-Exchange (EKE) protocol of Bellovin and Merritt in the ideal-cipher model. They define EKE2, which is a secure AKE protocol that provides forward secrecy. The protocol uses a Diffie-Hellman key exchange, where each flow is encrypted using the password. The shared session key is derived from a hash of the client and server identities and the exchanged values. The protocol also defines session IDs and partner IDs to ensure proper partnering and session freshness. The paper also discusses the addition of authentication to AKE protocols. It presents transformations that can be applied to an AKE protocol to provide client-to-server authentication, server-to-client authentication, or mutual authentication. These transformations use the distributed session key to construct an authenticator for the other party. The authors show that these transformations preserve the security properties of the original AKE protocol. The paper concludes with a discussion of ongoing work, including the analysis of EKE2 in the ideal-cipher model and the investigation of its security when the encryption function is instantiated with a random oracle. The authors also highlight the importance of considering the password space size in the context of dictionary attacks and the need for a robust model to capture the security requirements of password-based protocols.