Bridging the SSI Availability Gap — 层级式社会恢复 + 同意引擎 + 离线生存模式。从 3 分到 6 分，跨过四个评审轮次。
威胁模型、访问结构、状态机都有了。范围缩减到 3 个紧密集成的模块。评审对修士层面没有致命疑虑。
✓ 大概率够用
需要一个完成度验证件：ProVerif 模型证明撤销主导性，或原型消融实验证明 TTL 执行防止同意泄漏。
✗ 还差一步
形式化"默认过期"是设计原则贡献
但增量性仍受质疑
威胁模型、访问结构、共谋分析有了
但推导假设太强
N=24 可行但偏薄
ProVerif 承诺了还没交付
25 个弱点中，前 5 个不修就是废稿。
安全关键架构却不定义攻击者能做什么——阈值和降级策略全是任意的。
"≥2 层的 3 份"不是标准 (t,n) Shamir。访问结构允许弱组合：机构 + 被胁迫联系人 + 纸质备份。
Tier 2 联系人 + Tier 3 机构可以共谋。没有定量边界——多少守护者共谋后系统仍安全？
Normal/Caution/Emergency 没有状态机、触发阈值、退出条件。"降低阈值"本身是安全漏洞。
没有离线撤销列表、可信时间源（时钟回滚攻击）、>72h 紧急模式降低阈值是安全漏洞。
每个状态有不变量表、触发阈值、转换条件。确定性——给定 (counter, last_sync) 就能确定当前状态。
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 验证承诺是非强制的 → 评审标记为"承诺不是证据"。不变量是定义而非证明。安全概率假设独立性（q₂=0.05, q₃=0.005）太强。
形式化 ≠ 证明。定义 ≠ 验证。三个不变量说"规则是这样，所以性质成立"——但所有状态、缓存、离线模式、恢复路径是否真的保持这些性质，没有证明。
三个不变量本质上是自引用的：规则说 Revoked(c) → ¬Accept(c)，但 Ask: 在所有缓存状态、离线模式、恢复路径下，这条规则真的始终成立吗？
最小修复：转换规则表 + 归纳保护性论证，或 ProVerif/Tamarin 完成一个属性
P[attacker] ≈ O(10⁻⁵) 基于 q₂=0.05、q₃=0.005 的独立性假设。社会工程攻击通常相关——家人共享设备、居民同区域。
最小修复：明确假设章节 + 相关性分析，或实证校准数据
不需要更多的表。需要一个真正的验证。
ProVerif 模型
验证撤销主导性 + 一个失败案例
移除 TTL 执行模块，对比同意泄漏率。可测量改进 > 形式化声明。
所有状态转换规则 + 归纳论证：不变量在每个转换后保持。2-3 页足够。