该论文对Matrix协议的核心组件——设备导向的群组消息系统——进行了正式密码学分析。Matrix是一种去中心化的实时通信协议，广泛应用于安全即时通讯场景。作者通过建立精确的安全模型，定义了设备导向群组消息的密码学目标（如端到端加密、前向安全性、后向安全性和组内一致性），并证明了Matrix当前设计在某些假设下能够满足这些安全属性。分析揭示了协议中可能存在的细微安全假设依赖，并提出了改进建议。该研究为理解Matrix协议的安全性提供了严格的理论基础，并有助于指导未来群组通信协议的设计与验证。