1. 引言
密碼管理器（PM）是產生與儲存強隨機密碼的重要工具，用以應對密碼驗證中的弱點。然而，使用者信任仍是採用上的障礙。本文提出一個使用EasyCrypt證明環境的隨機密碼產生器（RPG）形式化驗證參考實作，重點在於功能正確性與安全性屬性。
2. 目錄
3. 現有密碼生成演算法
作者研究了15個密碼管理器，重點關注三個廣泛使用的開源軟體：Google Chrome（v89.0.4364.1）、Bitwarden（v1.47.1）和KeePass（v2.46）。這些軟體因其普及性與原始碼可取得性而被選中。
3.1 密碼組成政策
密碼管理器允許使用者定義密碼組成政策，包括長度、字元類別（小寫字母、大寫字母、數字、特殊字元）、每組的最小/最大出現次數、排除相似字元以及自訂字元集。表1總結了Chrome、Bitwarden和KeePass的政策。
3.2 隨機密碼生成
核心演算法從定義的字元集中生成隨機字元，直到達到密碼長度，並遵守最小/最大出現次數的限制。Chrome的演算法首先從具有最小出現次數的字元集中生成字元，然後從所有未超過最大值的字元集聯集中生成，最後對字串進行排列。
4. 形式化驗證框架
4.1 EasyCrypt概述
EasyCrypt是一個用於密碼學安全性證明的證明助手，採用基於遊戲的方法。它允許指定參考實作，並對功能正確性與安全性屬性進行形式化驗證。
4.2 安全性屬性
形式化定義包括隨機均勻性、抵抗側通道攻擊以及遵守政策限制等屬性。基於遊戲的方法模擬了敵手的能力，並證明了與理想隨機生成的不可區分性。
5. 技術細節與數學表述
密碼產生器的安全性使用計算不可區分性的概念來建模。令 $\mathcal{G}$ 為密碼生成演算法，$\mathcal{U}$ 為均勻隨機生成器。敵手 $\mathcal{A}$ 的優勢定義為：
$$\text{Adv}_{\mathcal{G}}(\mathcal{A}) = |\Pr[\mathcal{A}^{\mathcal{G}} = 1] - \Pr[\mathcal{A}^{\mathcal{U}} = 1]|$$
目標是證明對於所有機率多項式時間敵手，$\text{Adv}_{\mathcal{G}}(\mathcal{A})$ 是可忽略的。在EasyCrypt中的形式化證明涉及構建一系列遊戲，每個遊戲與前一個略有不同，並限制敵手成功機率的差異。
6. 實驗結果與圖表
形式化驗證是在密碼產生器的參考實作上進行的。證明包含約500行EasyCrypt程式碼，涵蓋功能正確性（生成的密碼滿足政策）和安全性（輸出與均勻隨機不可區分）。在標準筆記型電腦上，證明時間少於10秒。基於遊戲的證明結構圖如下所示：
圖1： 基於遊戲的證明結構：遊戲0（真實演算法）→ 遊戲1（將PRG替換為隨機）→ 遊戲2（將字元選擇替換為均勻）→ 遊戲3（理想）。每個轉換都由密碼學假設或歸約來證明其合理性。
7. 分析框架範例
案例研究：驗證KeePass密碼生成
考慮一個政策，要求一個12字元的密碼，其中至少包含2個小寫字母、2個大寫字母、2個數字和2個特殊字元。在EasyCrypt中的形式化規範定義了：
- 前置條件： 政策參數（長度、每組最小/最大值、排除字元）。
- 後置條件： 生成的密碼滿足所有限制，並且在有效密碼集合上是均勻隨機的。
- 安全性： 沒有敵手可以將輸出與相同長度的真正隨機字串區分開來。
證明透過對密碼長度進行歸納，顯示每個字元都是從適當的集合中均勻抽取的，並且最終的排列確保了沒有位置偏差。
8. 原始分析
核心見解： 本文透過將形式化驗證應用於密碼生成演算法，解決了密碼管理器信任中的一個關鍵缺口。雖然許多密碼管理器聲稱具有安全性，但很少有提供數學保證。使用EasyCrypt是朝向可證明安全的密碼生成邁出的重要一步。
邏輯流程： 作者首先調查現有演算法，識別常見模式與潛在缺陷。然後提出一個參考實作，並使用基於遊戲的證明對其正確性和安全性進行形式化驗證。流程合乎邏輯：問題識別 → 解決方案設計 → 形式化驗證 → 影響。
優勢與缺陷： 優勢在於嚴謹的形式化方法，提供了超越典型測試的保證。然而，本文專注於單一參考實作，而非驗證Chrome、Bitwarden或KeePass的實際程式碼。這限制了實際影響。此外，證明假設了一個可信的隨機數生成器，這在所有的部署場景中可能不成立。正如Bellare和Rogaway（1993）在其關於隨機預言機的開創性工作中所指出的，理論模型與實際實作之間的差距仍然是一個挑戰。
可行見解： 對於密碼管理器開發者而言，採用像EasyCrypt這樣的形式化驗證工具可以增強信任並減少漏洞。對於研究人員而言，將此工作擴展到驗證實際的密碼管理器原始碼（例如，透過反編譯或符號執行）將非常有價值。使用者應要求密碼管理器提供者提供透明度和形式化保證。此方法與美國國家標準與技術研究院（NIST）在其密碼模組驗證指南中所倡導的更廣泛的形式化方法趨勢一致。
9. 未來應用與展望
形式化驗證框架可以擴展到密碼管理器的其他功能，例如密碼儲存和自動填寫。與持續整合管線的整合可以實現密碼生成程式碼的自動驗證。未來的工作也可能探索側通道抵抗和量子安全隨機生成。隨著密碼管理器變得無所不在，形式化保證對於建立使用者信任和滿足法規要求（例如GDPR、eIDAS）將至關重要。
10. 參考文獻
- Bellare, M., & Rogaway, P. (1993). Random oracles are practical: A paradigm for designing efficient protocols. Proceedings of the 1st ACM Conference on Computer and Communications Security, 62-73.
- Barthe, G., et al. (2011). EasyCrypt: A tutorial. Foundations of Security Analysis and Design VII, 146-204.
- NIST. (2020). Cryptographic Module Validation Program (CMVP). National Institute of Standards and Technology.
- Shoup, V. (2004). Sequences of games: A tool for taming complexity in security proofs. IACR Cryptology ePrint Archive, 2004/332.
- Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Towards Formal Verification of Password Generation Algorithms used in Password Managers. arXiv:2106.03626v2.