Formal Verification of Password Generation Algorithms used in Password Managers

Abstract

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 work, we focus on a feature that most password managers offer that might impact the user’s trust, which is the process of generating random passwords. We survey which algorithms and protocols are most commonly used and we propose a solution for a formally verified reference implementation of a password generation algorithm. Finally, we realize this reference implementation in Jasmin and we prove that the concrete implementation preserves the verified properties. We use EasyCrypt as our proof framework and Jasmin as our programming language.