Bridging the SSI Availability Gap — 层级式社会恢复 + 同意引擎 + 离线生存模式。GPT-5.5 硬核评审 4 轮，从 3 分到 6 分的完整轨迹。
形式化"默认过期"是设计原则贡献，但增量性仍受质疑
威胁模型、访问结构、共谋分析有了，但推导假设太强
N=24 可行但偏薄；ProVerif 承诺了还没交付
TTL 重置缺陷完全修复（Round 1 → 2）；攻击概率从"拍脑袋"到正式推导 + 敏感度分析（Round 2 → 3）；三个安全不变量 + 最坏情形分析（Round 3 → 4）
一个真正的正确性证明。形式化不等于证明 — ProVerif 模型或原型消融实验，二者选一。
GPT-5.5 用 NeurIPS/ICML 级评审标准打出的 25 个弱点中，前 5 个是致命的。
整个架构是安全关键的，但没定义攻击者能做什么。没有威胁模型，阈值和降级策略都是任意的。
"≥2 层的 3 份"不是标准 (t,n) Shamir 能表达的。访问结构允许弱组合（机构 + 被胁迫联系人 + 纸质备份）。
Tier 2 两个联系人 + Tier 3 机构可以共谋。没有定量边界——多少比例的守护者可以共谋后系统仍然安全？
Normal/Caution/Emergency 没有状态机，没有触发阈值，没有恢复条件。"降低阈值"本身是安全漏洞。
没有离线撤销列表，没有可信时间源（时钟回滚攻击），>72h "紧急模式降低阈值"是安全漏洞。
每个状态有明确的不变量表、触发阈值、转换条件。确定性状态——给定（计数器，上次同步）就能确定当前状态。
Accept(c) ⟺ VerifySig ∧ NotExpired ∧ Fresh(status, c, Δ)。单调计数器替代挂钟，7d 硬拒绝，撤销列表必查。
3 个完整场景的消息序列图：正常同意授予+离线使用、紧急恢复+重新授权、撤销凭证/过期拒绝。每个场景有消息格式、状态转换、失败处理。
完整参数表、可用性推导 P[recovery]≈0.96、攻击概率上界 O(10⁻⁵)、5 种场景敏感度分析、正式安全定理。
① 撤销主导：Revoked(c) → ¬Accept(c)
② 过期拒绝：age(c) ≥ Δ_danger → 永不接受
③ 跨层恢复安全：|tiers(S)| ≥ 2 结构性保证
ProVerif 验证承诺是非强制的 → 评审标记为"承诺不是证据"。不变量是定义而非证明。安全概率假设太强（独立性、无相关性）。
从"承诺"到"证据"的距离。不需要更多形式化表，需要一个真正的正确性证明。
三个不变量本质上在说"规则是这样定义的，所以性质成立"。硬核部分——所有状态、缓存、离线模式、恢复路径是否真的保持这些性质——没有证明。
最小修复：转换规则表 + 归纳保护性论证，或 ProVerif/Tamarin 完成一个属性
P[attacker] ≈ O(10⁻⁵) 基于 q₂=0.05、q₃=0.005 的独立性假设。社会工程攻击通常相关（家人、共享设备）。结构性保证有意义但实践攻击可能跨层。
最小修复：明确假设章节 + 相关性分析，或实证校准数据
不需要更多的表。需要一个真正的验证。
ProVerif 模型
验证撤销主导性 + 一个失败案例
移除任一模块的 TTL 执行（恢复/离线/同意），对比同意泄漏率。可测量的改进 > 形式化声明。
写出所有状态转换规则 + 归纳论证：不变量在每个转换后保持。2-3 页足够。