矩阵重制：矩阵密码套件的机械化形式化分析

像 WhatsApp、Facebook Messenger、Matrix 和 Signal 应用等安全即时群组 messaging 应用在当今互联网中已广泛普及, 累计服务数十亿用户。与 WhatsApp 不同, Matrix 可以以联邦方式部署, 允许用户选择管理其聊天的服务器。为此, Matrix 采用两种新型密码协议: Olm 用于保护成对通信, Megolm 依赖于 Olm 用于保护群组通信。Olm 和 Megolm 与 Signal 和 Sender Keys 在安全目标上类似, 且已在实际中广泛部署以保护群组通信。虽然 Olm、Megolm 和 Sender Keys 已在计算模型中进行了手工分析, 但尚无符号化分析或正确性机械化证明。机械化证明和计算机辅助分析对于密码协议至为重要, 因为手写证明和分析容易出错且常常包含细微之误。我们使用 Verifpal 构建了 Olm 和 Megolm 以及它们的组合的形式化模型。我们对 Olm 和 Megolm 的各种感兴趣的属性进行了证明, 包括身份验证、机密性、前向安全性和后竞争安全性。我们还机械化了已知的局限性、先前发现的攻击以及来自规格和先前文献的平凡攻击者胜利。最后, 我们对 Sender Keys 以及 Signal 与 Sender Keys 的组合进行建模, 以便与 Olm、Megolm 及其组合进行比较。通过我们的分析, 我们得出结论:如果 Olm 预密钥被签名, 则 Olm 和 Megolm 的组合与 Signal 和 Sender Keys 的组合在安全性上相当;但如果 Olm 预密钥未被签名, 则 Olm 和 Megolm 的组合在后竞争安全性上证明性地更差。