近年来，端到端加密消息传递已成为主流。用户期望他们的对话是私密的，并且只有预期的接收者才能阅读。为了满足这一需求，信号协议成为了一个广受欢迎的选择，许多消息应用程序都采用了它。

最近，Apple 发布了他们定制的后量子 (Post-Quantum, PQ) 密钥协商协议 PQ3，用于 iMessage。 PQ3 旨在提供比其前身更强的安全性，尤其是针对潜在的量子计算机攻击。

本文档提供了一个对 Apple PQ3 协议的形式化分析。我们的分析利用形式化方法来验证协议的安全性属性，例如身份验证和密钥协议。 通过应用形式化验证技术，我们旨在对 PQ3 协议的安全性提供严格的保证，并识别任何潜在的漏洞或弱点。

我们相信这项工作对于更广泛的密码学社区和对安全消息传递系统感兴趣的人来说都很有价值。我们的分析有助于理解 PQ3 协议的优势和局限性，并为安全协议的设计和验证提供见解。