1. 引言
密碼管理器係現代數碼安全嘅重要工具，令用戶無需記住複雜密碼，都可以使用強而獨特嘅密碼。儘管佢咁重要，但由於信任問題，用戶採用率仍然有限。本文針對一個關鍵嘅信任組成部分：隨機密碼生成演算法。我哋提出一個使用EasyCrypt框架進行形式化驗證嘅參考實現，透過基於博弈嘅密碼學證明，驗證功能正確性同安全屬性。
2. 現行密碼生成演算法
本研究檢視咗15個密碼管理器，重點分析三個開源實現：Google Chrome (v89.0.4364.1)、Bitwarden (v1.47.1) 同 KeePass (v2.46)。選擇呢啲係因為佢哋廣泛使用同源代碼易於取得。
2.1 密碼組成策略
密碼管理器允許用戶定義生成密碼必須滿足嘅組成策略。呢啲策略控制密碼長度、字元類別，以及特定限制，例如每類字元嘅最少/最多出現次數，同排除相似字元（例如 'l'、'I'、'O'、'0'）。
策略比較
- Chrome: 長度：1-200，集合：小寫字母、大寫字母、字母、數字、特殊字元
- Bitwarden: 長度：5-128，集合：小寫字母、大寫字母、數字、特殊字元
- KeePass: 長度：1-30000，集合：小寫字母、大寫字母、數字、特殊字元、括號、空格、減號、底線
2.2 隨機密碼生成
調查嘅演算法遵循相似模式：從唔同字元集生成隨機字元，直到滿足密碼長度要求，同時遵守最少同最多出現次數限制。Chrome嘅演算法具體步驟：1) 從設有最少出現次數嘅集合生成字元，2) 從未達到最多出現次數嘅集合聯集中生成字元，3) 應用最終排列。
3. 形式化驗證框架
我哋採用EasyCrypt呢個用於密碼學協議嘅證明輔助工具，來形式化指定同驗證我哋嘅參考RPG實現。驗證遵循基於博弈嘅密碼學安全證明方法，建立均勻分佈同抵禦預測攻擊等屬性。
核心見解
- 形式化驗證提供關於演算法行為嘅數學確定性
- 基於博弈嘅證明能現實地模擬攻擊者能力
- 參考實現可作為密碼管理器開發者嘅黃金標準
4. 技術實現細節
4.1 數學基礎
密碼生成演算法必須確保喺定義嘅密碼空間內均勻分佈。對於一個允許使用大小為$|C|$嘅字元集$C$，並要求長度為$L$嘅策略，總密碼空間大小為$|C|^L$。演算法必須保證每個可能嘅密碼$p \in C^L$都有相等概率：
$$\Pr[\text{Generate}(L, C) = p] = \frac{1}{|C|^L}$$
當加入最少出現次數等限制時，分佈會變成條件性，但必須喺受限制嘅空間內保持均勻。
4.2 安全屬性
形式化驗證嘅屬性包括：
- 功能正確性： 輸出滿足所有策略限制
- 均勻分佈： 密碼選擇無偏差
- 抵禦預測： 先前輸出唔會揭示未來輸出
- 熵保持： 保持密碼學隨機性
5. 實驗結果
形式化驗證嘅實現對比咗三個研究嘅密碼管理器進行測試。主要發現：
- 所有商業實現喺邊緣情況下都顯示出輕微統計偏差
- KeePass展示咗最靈活嘅策略系統，但複雜性帶來驗證挑戰
- Bitwarden嘅實現最接近理想均勻分佈
- Chrome嘅演算法喺驗證方面有最清晰嘅關注點分離
統計分佈分析
測試涉及為每個配置生成1,000,000個密碼，並應用χ²測試驗證均勻性。經驗證嘅實現通過所有統計測試 (p > 0.05)，而商業實現喺特定策略配置下顯示p值低至0.001，表明存在可檢測嘅偏差。
6. 分析框架示例
核心見解： 本文嘅根本突破唔只係另一個密碼生成器——而係建立咗一個驗證方法論，將安全性從經驗聲明轉變為數學證明。呢個將範式從「我哋認為佢安全」轉變為「我哋可以證明佢安全」。
邏輯流程： 研究遵循清晰嘅三階段論證：1) 透過用戶研究確定信任係採用瓶頸，2) 解構現有實現以尋找值得驗證嘅通用模式，3) 構建並證明一個可作為信任錨嘅參考實現。呢個方法同基礎性著作如Verified Software Initiative中嘅方法相似，將形式化方法應用於實際安全問題。
優點與不足： 優點在於喺正確嘅抽象層次處理驗證問題——專注於生成演算法而非整個密碼管理器。然而，本文嘅限制係孤立地處理生成器。正如NIST嘅Digital Identity Guidelines所指，密碼安全取決於整個生態系統：儲存、傳輸同UI/UX。如果密碼透過側信道或差劣嘅UI設計洩漏，一個形式化驗證嘅生成器都係無用嘅。
可行見解： 密碼管理器開發者應該：1) 採用呢個參考實現作為起點，2) 將驗證擴展到密碼儲存同自動填充組件，3) 委託第三方使用呢個方法論進行審計。呢個方法可以擴展到其他安全關鍵嘅生成器（密碼學金鑰、會話令牌），跟隨經驗證嘅密碼學庫如HACL*所建立嘅模式。
呢個300-600字嘅分析展示咗形式化驗證如何解決密碼管理器嘅核心信任赤字。透過提供安全屬性嘅數學證明，呢項工作超越咗啟發式安全，邁向可證明嘅保證。方法論嘅真正價值在於其可轉移性——相同技術可以驗證其他安全組件，建立一條從密碼生成到儲存再到使用嘅信任鏈。呢個同驗證系統嘅更廣泛趨勢一致，正如seL4微內核驗證等項目所見，證明形式化方法對於現實世界安全系統正變得實用。
7. 未來應用與方向
呢度建立嘅形式化驗證方法論有幾個有前景嘅應用：
- 標準化： 可作為密碼生成器認證標準嘅基礎
- 瀏覽器整合： 所有主要瀏覽器內置經驗證嘅密碼生成器
- 物聯網安全： 用於嵌入式設備嘅輕量級經驗證生成器
- 無密碼認證： FIDO2/WebAuthn令牌生成器嘅驗證
- 教育工具： 透過實際安全示例教授形式化方法
未來研究應專注於：1) 將驗證擴展到密碼策略評估，2) 與硬件安全模組整合，3) 為密碼管理器開發者開發自動化驗證工具，4) 研究形式化驗證系統對可用性嘅影響。
8. 參考文獻
- Grilo, M., Ferreira, J. F., & Almeida, J. B. (2021). Towards Formal Verification of Password Generation Algorithms used in Password Managers. arXiv:2106.03626
- EasyCrypt: Computer-Aided Cryptographic Proofs. (2021). https://easycrypt.info/
- NIST. (2020). Digital Identity Guidelines: Authentication and Lifecycle Management. SP 800-63B
- Klein, G., et al. (2009). seL4: Formal verification of an OS kernel. SOSP '09
- Zinzindohoué, J. K., et al. (2017). HACL*: A Verified Modern Cryptographic Library. CCS '17
- Bonneau, J., et al. (2012). The quest to replace passwords: A framework for comparative evaluation of web authentication schemes. IEEE S&P
- Ur, B., et al. (2016). "I added '!' at the end to make it secure": Observing password creation in the lab. SOUPS '16