XiaoMi-AI文件搜索系统
World File Search SystemiMessage
对苹果的iMessage PQ3协议的正式分析
我们介绍了Apple的Imessage PQ3的正式验证，这是一种高性能，设备到设备的消息传递协议，即使对具有量子计算功能的对手，也提供了强大的安全保证。PQ3利用苹果的身份服务以及定制的，量子后安全的初始化阶段，之后它采用信号风格的双棘轮构造，扩展以提供量子后，后弹力后的安全性。我们提出了PQ3的详细正式模型，它是其细粒度安全属性的精确规格，并使用T amarin Prover进行了机器检查的安全性证明。特别是新颖的是将量子后安全键的整合到相关协议阶段以及详细的安全要求以及其完整的正式分析中。我们的分析涵盖了两个关键棘轮，包括无界循环，某些循环被认为是诸如T amarin这样的符号掠夺的范围（不是！）。
iMessage PQ3协议安全性分析
iMessage PQ3 协议是一种端到端加密消息传递协议，旨在在两个设备之间的长期会话中交换数据。它旨在为前向保密和后泄露保密以及经典身份验证提供经典和后量子机密性。其初始认证密钥交换由数字签名加上椭圆曲线 Diffie-Hellman 和后量子密钥交换构成；为了持续派生每条消息的密钥，它采用了 Signal 双棘轮的改编，其中包括后量子密钥封装机制。本文介绍了 PQ3 协议的加密细节，并通过改编 Cohn-Gordon 等人对 Signal 的多阶段密钥交换安全性分析给出了还原论安全性分析。(J. Cryptology，2020)。分析表明，PQ3 在协议的初始密钥交换以及持续密钥更新阶段均提供了具有前向保密性的机密性和针对传统和量子对手的后泄露安全性。