Towards Formal Verification of Password Generation Algorithms used in Password Managers

2021/06/07 by Miguel L. Grilo, Grilo, Miguel, João F. Ferreira +3
Computer Science · #User Authentication and Security Systems #Advanced Malware Detection Techniques #Advanced Authentication Protocols Security

paper · pdf · doi:10.48550/arxiv.2106.03626

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 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.

Related

• Secure Password Generator Based on Secure Pseudo-Random Number Generator
• That Was Then, This Is Now: A Security Evaluation of Password Generation, Storage, and Autofill in Thirteen Password Managers
• Trenchcoat: Human-Computable Hashing Algorithms for Password Generation
• Are Users More Willing to Use Formally Verified Password Managers?
• Password Generators: Old Ideas and New