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.

In the symbolic verification of cryptographic protocols, a central problem is deciding whether a protocol admits an execution which leaks a designated secret to the malicious intruder. In [1], it is shown that, when considering finitely many sessions, this “insecurity problem” is NP-complete. Central to their proof strategy is the observation that any execution of a protocol can be simulated by one where the intruder only communicates terms of bounded size. However, when we consider models where, in addition to terms, one can also communicate logical statements about terms, the analysis of the insecurity problem becomes tricky when both these inference systems are considered together. In this paper we consider the insecurity problem for protocols with logical statements that include equality on terms and existential quantification. Witnesses for existential quantifiers may be unbounded, and obtaining small witness terms while maintaining equality proofs complicates the analysis considerably. We extend techniques from [1] to show that this problem is also in NP.

Abstract We study procedures for the derivability problem of fragments of intuitionistic logic. Intuitionistic logic is known to be PSPACE-complete, with implication being one of the main contributors to this complexity. In fact, with just implication alone, we still have a PSPACE-complete logic. We study fragments of intuitionistic logic with restricted implication and develop algorithms for these fragments which are based on the proof rules. We identify a core fragment whose derivability is solvable in linear time. Adding disjunction elimination to this core gives a logic which is solvable in co-NP. These sub-procedures are applicable to a wide variety of logics with rules of a similar flavour. We also show that we cannot do better than co-NP whenever disjunction elimination interacts with other rules.