Secure communication and authentication in the Internet of Medical Things (IoMT) are critical for patient safety and healthcare data protection, yet existing protocols face significant vulnerabilities that remain undetected by conventional verification approaches. This paper presents the computational security verification of an IoMT authentication protocol incorporating NTRU lattice-based post-quantum cryptography using CryptoVerif, a formal verification tool that provides concrete probability bounds under standard cryptographic assumptions. Through systematic analysis of a multi-entity healthcare protocol, this study identifies two critical security flaws overlooked by previous symbolic verification methods: device registration authentication failure enabling man-in-the-middle device substitution attacks, and forward secrecy violation through static key encryption that exposes historical medical data upon key compromise. To address these vulnerabilities, we provide an enhanced protocol incorporating Strong Unforgeability under Chosen Message Attacks (SUF-CMA) MAC-based device authentication that cryptographically binds device identity to patient identity, and HMAC-based key derivation function (HKDF)-derived ephemeral session keys that achieve forward secrecy through fresh key derivation for each communication session. Our CryptoVerif implementation successfully proves nine security properties including mutual authentication, data confidentiality, device binding, and forward secrecy, with aggregate security bound for 128-bit quantum-resistant security. Unlike symbolic verification tools that assume perfect cryptography, our computational analysis provides concrete security guarantees essential for safety-critical healthcare systems.
