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.

The proliferation of Internet-of-Things (IoT) devices in critical infrastructure requires robust security mechanisms to verify device integrity and trustworthiness. Remote Attestation (RA) is a security mechanism for validating the software and hardware state of remote devices. Existing RA solutions for resource-constrained IoT devices lack comprehensive frameworks for secure attestation channels and focus primarily on local evidence generation without addressing end-to-end security. This paper introduces M-AuRA, a lightweight RA solution that fills these gaps by leveraging the newly standardized Ephemeral Diffie-Hellman over COSE (EDHOC) protocol. M-AuRA seamlessly integrates attestation with authentication, enabling both unilateral and mutual attestation modes while maintaining minimal resource overhead. Our framework specifies how to transport existing attestation mechanisms in parallel with secure communication establishment, providing a complete end-to-end security solution for IoT deployments. We demonstrate M-AuRA’s practicality through implementation on the nRF5340 microcontroller running at 64 MHz, evaluating performance across both software and hardware cryptographic back-ends. In mutual attestation mode, our implementation uses only 4,692 B RAM and 19,350 B flash memory, occupying 0.9% and 1.85% of available nRF5340 resources, respectively. The four-message EDHOC exchange (45 B, 65 B, 177 B and 120 B) enables mutual trustworthiness verification in 10.46 s using a software-based cryptographic back-end, or only 0.43 s with hardware acceleration, consuming 171.43 mC and 7.97 mC of charge, respectively.

This paper explores preliminary research on improving the Ephemeral Diffie-Hellman Over COSE (EDHOC) protocol by incorporating a new pre-shared key (PSK) authentication method. The research focuses on designing this PSK-based mechanism and its potential benefits, such as enhancing session key update efficiency and reducing computational demands compared to current EDHOC authentication methods. We also outline the planned implementation and evaluation approach, which will measure key performance indicators like memory consumption, energy consumption, handshake duration, message size or number of operations. The aim is to optimize EDHOC for secure communication in resource-limited environments.