  Password managers are important tools that enable us to use stronger
passwords, freeing us from the cognitive burden of remembering them. Despite
this, there are still many users who do not fully trust password managers. In
this paper, we focus on a feature that most password managers offer that might
impact the user's trust, which is the process of generating a random password.
We survey which algorithms are most commonly used and we propose a solution for
a formally verified reference implementation of a password generation
algorithm. We use EasyCrypt as our framework to both specify the reference
implementation and to prove its functional correctness and security.
