1. Signal Protocol and Post-Quantum Ratchets (signal.org)
Signal 协议与后量子棘轮
Signal 协议是为数十亿用户提供端到端加密的通信标准。为应对未来量子计算机可能带来的威胁（特别是“先收集，后解密”攻击），Signal 引入了稀疏后量子棘轮，将其与现有的双重棘轮结合，形成三重棘轮协议。此升级旨在不损害现有前向保密和后向安全保障的前提下，实现抗量子安全性，且对用户无感知。
问题背景与现有安全机制
- 量子威胁：现有协议依赖椭圆曲线密码学，该密码学不具备抗量子性。未来的量子计算机可能破解这些密钥，破坏通信安全。
- 现有保护：Signal 双重棘轮通过哈希函数（抗量子）提供前向保密，通过椭圆曲线迪菲-赫尔曼密钥交换提供后向安全。棘轮机制确保密钥只能单向更新，即使当前密钥泄露，也能保护过去（前向保密）和未来（后向安全）的消息。
- 先前改进：PQXDH 协议在会话建立阶段加入了抗量子秘密，以保护会话初始材料，但无法保护会话持续过程中的密钥更新。
解决方案：三重棘轮与 SPQR
- 核心思路：在运行现有双重棘轮的同时，引入一个额外的后量子棘轮。两个棘轮独立运行并生成密钥，最终通过密钥派生函数混合，形成最终的消息加密密钥。攻击者必须同时破解椭圆曲线和后量子密码才能获得有效密钥。
- 后量子棘轮工具：采用密钥封装机制，特别是标准化的ML-KEM算法。与迪菲-赫尔密钥交换不同，KEM 需要有序、不对称的消息交换（发送封装密钥，接收密文）。
- 设计挑战：直接集成 KEM 会带来问题：密文尺寸大（>1000字节 vs. ECDH的32字节）会增加带宽成本；在处理离线、丢包、乱序及恶意中间人干扰时需保持鲁棒性。
SPQR 的关键技术设计
为高效、安全地集成 KEM，SPQR 采用了以下设计：
- 状态机管理：通信双方维护状态机（如
StartingA,SendEK,SendingCT），协调密钥交换数据的发送与接收，确保协议有序进行。 - 带宽优化与抗干扰：
- 问题：直接发送完整大尺寸的封装密钥和密文不现实。
- 擦除码分块：将大块数据（如封装密钥）拆分为多个小块，并使用擦除码技术。接收方只需收到任意足够数量的分块即可重构原始数据。这解决了丢包和乱序问题，并迫使恶意中间人必须丢弃几乎所有分块（导致明显的服务中断）才能成功干扰，大幅提高了攻击成本。
- 高效密钥交换（ML-KEM Braid）：通过深入分析 ML-KEM 算法流程，将其分解为多个可并行传输的阶段。例如，将封装密钥的部分（如种子和哈希值）先发送，允许接收方提前开始生成密文的大部分，从而充分利用消息的发送能力，在更短时间内完成秘密共享，同时避免过早生成过多未使用的密钥材料而损害安全性。
部署策略与兼容性
- 透明升级：对用户而言，使用体验无变化。升级将在后台自动完成。
- 渐进式部署：采用异构推出策略。新客户端首次与旧客户端通信时，SPQR 数据附带在消息中但不用于加密。若对方不支持，则仅在此会话的初始阶段回退到不使用 SPQR。此降级机制受消息认证码保护，可防止恶意降级，且仅在会话开始时发生一次，之后即锁定。
- 未来计划：待所有客户端均支持新协议后，将强制要求所有会话使用 SPQR，淘汰旧会话，实现全覆盖。
正确性与安全性保障
- 形式化验证：协议设计早期就与学术界合作，并使用 ProVerif 进行建模和证明，确保其具备所需的安全属性。
- 实现验证：使用 hax 工具将 Rust 实现自动翻译为 F* 语言，并在持续集成中证明：核心功能正确性、函数前后条件满足、整个代码库无恐慌。这确保了实现的健壮性和与形式化模型的一致性。
- 持续保障：形式化验证集成到开发流程中，每次代码提交都会运行验证，确保质量不随迭代而下降。
总结
Signal 通过引入 SPQR 构建三重棘轮协议，在保持现有顶级安全标准的同时，前瞻性地为通信提供了量子安全保护。该方案设计精巧，注重效率（控制带宽开销）和鲁棒性（抗恶意干扰与丢包），并通过严谨的形式化方法保证了从协议设计到代码实现的可靠性。此次升级对用户透明，但为应对未来的量子计算威胁奠定了坚实基础。