The adoption of security protocols such as Transport Layer Security (TLS) has significantly improved the state of traffic encryption and integrity protection on the Internet. Despite rigorous analysis, vulnerabilities continue to emerge, sometimes due to fundamental flaws in the protocol specification. This paper examines the security of TLS when using Raw Public Key (RPK) authentication. This mode has not been as extensively studied as X.509 certificates and Pre-Shared Keys (PSK). We develop a formal model of TLS RPK using applied pi calculus and the ProVerif verification tool, revealing that the RPK mode is susceptible to identity misbinding attacks. Our contributions include formal models of TLS RPK with several mechanisms for binding the endpoint identity to its public key, verification results, practical scenarios demonstrating the misbinding attack, and recommendations for mitigating such vulnerabilities. These findings highlight the need for improved security measures in TLS RPK.

翻译：传输层安全（TLS）等安全协议的采用显著改善了互联网流量加密与完整性保护的状况。尽管经过严格分析，漏洞仍不断出现，有时源于协议规范中的根本性缺陷。本文研究了使用原始公钥（RPK）认证时TLS的安全性。相较于X.509证书与预共享密钥（PSK），该模式尚未得到充分研究。我们运用应用π演算与ProVerif验证工具建立了TLS RPK的形式化模型，揭示出RPK模式易受身份错误绑定攻击。我们的贡献包括：建立了多种将端点身份与其公钥绑定机制下的TLS RPK形式化模型、验证结果、展示错误绑定攻击的实际场景，以及缓解此类漏洞的建议。这些发现凸显了改进TLS RPK安全措施的必要性。