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.

Digital ticketing systems typically offer ticket purchase, refund, validation, and, optionally, anonymity of users. However, it would be interesting for users to transfer their tickets, as is currently done with physical tickets. We propose Applause, a ticketing system allowing the purchase, refund, validation, and transfer of tickets based on trusted authority, while guaranteeing the anonymity of users, as long as the used payment method provides anonymity. To study its security, we formalise the security of the transferable E-Ticket scheme in the game-based paradigm. We prove the security of Applause computationally in the standard model and symbolically using the protocol verifier ProVerif. Applause relies on standard cryptographic primitives, rendering our construction efficient and scalable, as shown by a proof-of-concept. In order to obtain Spotlight, an auditable version, proved to be secure, users will remain anonymous except for a trusted third party, which will be able to disclose their identity in the event of a disaster.

International audience