论文对法国高官使用的 Olvid 通讯软件进行形式化安全分析

jedisct1 · x · 2026-08-07

研究人员对端到端加密通讯应用 Olvid 的密码学核心进行了首次形式化安全分析。该软件被法国政府官员广泛使用。

研究团队使用 Tamarin Prover 工具构建了详细的协议模型，验证了其在相互认证、会话密钥保密性和前向保密等方面的核心安全保证。然而，分析也揭示了其局限性：与现代安全协议（如 Signal）相比，Olvid 无法满足 eCK 等现代强安全模型的要求，并且存在潜在的时间泄漏风险。