EDHOC is a lightweight authenticated key exchange protocol designed for constrained IoT devices. It currently supports asymmetric authentication, either using digital signatures or static Diffie-Hellman (DH) keys. Since many IoT deployments rely on Pre-Shared Keys (PSK) for authentication, a new PSK-based authentication method (EDHOC-PSK) is currently under standardization. This paper presents a symbolic analysis EDHOC-PSK (draft version 06) using SAPIC+, which compiles a single formal specification into multiple state-of-the-art verification tools, including Tamarin and ProVerif. Our model extends the typical Dolev-Yao (DY) adversary with additional capabilities, including leakage of ephemeral secrets, leakage of the long-term Pre-Shared Key leakage of the session key and a discrete-logarithm oracle. We verify the confidentiality, authentication, and key-agreement properties stated in the draft, and we refine the specification of identity protection by distinguishing anonymity and unlinkability. We show that EDHOC-PSK achieves anonymity for both parties against active attackers, while unlinkability holds only for the Initiator under passive attackers. Finally, we analyze a post-quantum Store-Now-Decrypt-Later (SNDL) adversary and find that all proven properties remain intact except Perfect Forward Secrecy (PFS), which cannot be preserved once DH secrets are recoverable.
Proceedings of the ACM Asia Conference on Computer and Communications Security
2026-06
2026-06-23