摘要。我们形式描述,正式建模,并证明了Telegram对客户服务器通信的密钥交换协议的安全性。为了实现这一目标,我们开发了一个合适的多阶段密钥交换安全模型以及基于对电报的规格和客户端源代码的分析的电报协议的伪代码描述。我们仔细记录了我们的描述与现实有何不同并证明我们的建模选择合理性。我们的安全证明将协议的安全性降低到其加密构件的安全性,但是对这些构建块的随后分析需要引入许多新颖的安全假设,这反映了从正式分析的角度来看,电信作出的许多设计决策是次优的。在此过程中,我们为电报中使用的RSA-OEAP+变体提供了IND-CCA安全性证明,并确定利用当前Telegram服务器行为的假设攻击(在我们的协议描述中未捕获)。最后,我们反思有关协议设计的更广泛的教训,可以从我们的工作中获取。
主要关键词