Reassessing Forward Secrecy in a Lightweight Ascon-Based IoMT Authentication Protocol: Exposure-Boundary Analysis and Ephemeral Reinforcement

A forward-secrecy claim protects past sessions only against the compromise it assumes. In lightweight Internet of Medical Things (IoMT) authentication, devices may stay in service for years, and a server may store more than its master key. We compare six published schemes at the source level and find that in five of them the published equations allow a key protecting past sessions to be recomputed from the state retained by the server or gateway. We then examine a recently published Ascon-based IoMT protocol in detail. Its forward-secrecy discussion considers only disclosure of the master key, yet an attacker who also obtains the registration records can recompute the transcript-protection keys and reconstruct an accepted historical session key. A ProVerif experiment, in which compromise is triggered only after the tested session completes, produces an executable trace of this reconstruction. The protocol also reuses Ascon nonces with fixed keys, contrary to the NIST nonce-uniqueness requirement, and its message flow provides no reverse key confirmation. An authenticated ephemeral Diffie–Hellman or idealised key-encapsulation contribution blocks the reconstruction in the symbolic models, and a further variant, S4, adds reverse confirmation and transcript-identity hardening. All results are symbolic, and X25519 and ML-KEM-512 serve only as deployment and size references.