Towards Formal Verification of Password Generation Algorithms in Password Managers

1. Introduction

Password managers (PMs) are essential tools for enhancing security by enabling the use of strong, unique passwords without the cognitive burden of memorization. Despite their benefits, user trust remains a significant barrier to adoption. This paper addresses a critical feature that impacts trust: the random password generation algorithm. We propose a formally verified reference implementation using the EasyCrypt framework to prove both functional correctness and security properties, aiming to establish a trustworthy standard for password generation in PMs.

2. Current Password Generation Algorithms

The study surveyed 15 password managers, with detailed analysis focused on three widely-used, open-source examples: Google Chrome's Password Manager, Bitwarden, and KeePass. The goal was to understand common algorithms and identify areas for formal verification.

3. Formal Verification Approach

The paper employs the EasyCrypt proof assistant to formalize and verify the password generation algorithm. The verification focuses on two key properties:

• Functional Correctness: The algorithm always produces a password that satisfies the user-defined composition policy.
• Security (Randomness): The output password is computationally indistinguishable from a truly random string of the same length drawn from the policy-defined alphabet, assuming a cryptographically secure random number generator (CSPRNG). This is modeled using a game-based cryptographic proof approach.

This formal method moves beyond traditional testing, providing mathematical guarantees about the algorithm's behavior.

4. Technical Details and Mathematical Formulation

The security property is formalized as a cryptographic game. Let $\mathcal{A}$ be a probabilistic polynomial-time (PPT) adversary. Let $\text{Gen}(policy)$ be the password generation algorithm and $\text{Random}(policy)$ be an ideal generator that outputs a uniformly random string from all strings satisfying the $policy$. The advantage of $\mathcal{A}$ in distinguishing between them is defined as:

$\text{Adv}_{\text{Gen}}^{\text{dist}}(\mathcal{A}) = |\Pr[\mathcal{A}(\text{Gen}(policy)) = 1] - \Pr[\mathcal{A}(\text{Random}(policy)) = 1]|$

The algorithm is considered secure if this advantage is negligible for all PPT adversaries $\mathcal{A}$, meaning $\text{Adv}_{\text{Gen}}^{\text{dist}}(\mathcal{A}) \leq \epsilon(\lambda)$, where $\epsilon$ is a negligible function in the security parameter $\lambda$. The proof in EasyCrypt constructs a sequence of games (Game$_0$, Game$_1$, ...) to bound this advantage, often relying on the assumption that the underlying PRG is secure.

5. Experimental Results and Chart Description

While the PDF primarily focuses on the formal specification and proof strategy, the practical outcome is a verified reference implementation. The "experiment" is the successful completion of the formal proof in the EasyCrypt environment. This serves as a blueprint for correctness.

Conceptual Chart Description: A flowchart would effectively visualize the verified algorithm:

1. Start: User inputs policy (length L, character sets S1...Sn with min/max counts).
2. Step 1 - Fulfill Minimums: For each set Si with min_i > 0, generate min_i random characters from Si. Counter: $\sum min_i$ characters generated.
3. Step 2 - Fill to Length L: Let $\text{Remaining} = L - \sum min_i$. While Remaining > 0: Create a pool from all sets Si where current_count(Si) < max_i. Select a random character from this pool. Decrement Remaining.
4. Step 3 - Shuffle: Apply a cryptographically secure random permutation (Fisher-Yates shuffle) to the list of L characters.
5. Step 4 - Output: Output the final shuffled string. The green checkmark at this step is labeled "Formally Verified (EasyCrypt): Correctness & Randomness".

6. Analysis Framework: Example Case

Scenario: Verifying that the algorithm avoids a subtle bias when the "Exclude similar characters" option (e.g., excluding 'l', 'I', 'O', '0') is enabled.

Potential Flaw (Without Verification): A naive implementation might first generate a password from the full set and then remove excluded characters, potentially resulting in a shorter password or altering the distribution of the remaining character sets, violating the policy or introducing bias.

Formal Verification Approach: In EasyCrypt, we would specify the character set as $\text{Alphabet}_{\text{final}} = \text{Alphabet}_{\text{full}} \setminus \text{ExcludedSet}$. The proof would then demonstrate that the generation process (Steps 1 & 2 above) samples uniformly from $\text{Alphabet}_{\text{final}}$ for the relevant character sets, and that the minimum/maximum constraints are evaluated correctly against this reduced set. This eliminates the flaw by construction.

Non-Code Artifact: The formal specification in EasyCrypt for the character selection step would logically define the sampling pool, ensuring excluded characters are never part of the source.

7. Core Insight & Analyst's Perspective

Core Insight: The paper's fundamental contribution is shifting the trust model for password managers from "hopefully secure via code review and testing" to "mathematically proven secure via formal verification." It correctly identifies the password generator as a linchpin of trust—a single point of failure that, if flawed, undermines the entire security premise of the manager. This work is part of a crucial but underappreciated trend in applied cryptography, mirroring efforts like the formal verification of the TLS protocol (Project Everest) or cryptographic libraries (HACL*).

Logical Flow: The argument is sound: 1) User trust is low due to opaque security. 2) Password generation is a critical, complex component prone to subtle bugs (e.g., bias, policy violations). 3) Formal methods offer the highest assurance. 4) EasyCrypt provides a practical framework for this verification. 5) A verified reference implementation can serve as a gold standard for the industry.

Strengths & Flaws: Strengths: The focus on a concrete, high-impact problem is excellent. Using EasyCrypt, a mature tool for game-based proofs, is pragmatic. The analysis of real-world PM algorithms grounds the research in practice. Flaws: The paper is a "towards" paper—it lays the groundwork but doesn't present a complete, battle-tested verified implementation for all policies of a major PM. The real challenge is the complexity of commercial password policies (like KeePass's extensive options), which may explode the verification state space. It also sidesteps the elephant in the room: the security of the surrounding PM system (UI, memory, storage, auto-fill) is equally critical, as noted in studies by organizations like the NCC Group.