This paper addresses the problem of authenticated key exchange (AKE) in password-based protocols, where adversaries can enumerate all possible passwords. 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 and provide definitions for it and entity-authentication goals. The paper proves the security of the Encrypted Key-Exchange (EKE) protocol, which consists of two flows, in an ideal-cipher model, achieving forward secrecy. The contributions of the paper include: 1. **Model and Definitions**: They modify and extend the models and definitions from previous work to handle dictionary attacks, forward secrecy, and other security concerns. 2. **Security Proof**: They prove the security of EKE2, a two-flow protocol at the core of Bellovin and Merritt's EKE, in the ideal-cipher model, ensuring forward secrecy. 3. **Protocol Transformations**: They describe generic transformations to add client-to-server, server-to-client, and mutual authentication to AKE protocols. The paper also discusses the challenges and open problems in dealing with the complexity of proofs and the variety of protocol variants in this domain.This paper addresses the problem of authenticated key exchange (AKE) in password-based protocols, where adversaries can enumerate all possible passwords. 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 and provide definitions for it and entity-authentication goals. The paper proves the security of the Encrypted Key-Exchange (EKE) protocol, which consists of two flows, in an ideal-cipher model, achieving forward secrecy. The contributions of the paper include: 1. **Model and Definitions**: They modify and extend the models and definitions from previous work to handle dictionary attacks, forward secrecy, and other security concerns. 2. **Security Proof**: They prove the security of EKE2, a two-flow protocol at the core of Bellovin and Merritt's EKE, in the ideal-cipher model, ensuring forward secrecy. 3. **Protocol Transformations**: They describe generic transformations to add client-to-server, server-to-client, and mutual authentication to AKE protocols. The paper also discusses the challenges and open problems in dealing with the complexity of proofs and the variety of protocol variants in this domain.