Skip to content
Open access

MQTT-HS: A formally verified and proxy-mediated hybrid security protocol for MQTT-based IoT networks

Oct 2026 · Journal of King Saud University: Computer and Information Sciences · Vol 38 · 0 citations · 36 references

TL;DR

The results support the feasibility of MQTT-HS under the evaluated prototype configuration, and the modeled secrecy, authentication, replay-resistance, message-flow agreement, and epoch-key secrecy properties of the cryptographic core are verified.

Abstract

MQTT enables efficient communication in resource-constrained Internet of Things (IoT) systems but does not provide integrated protection against cryptographic and behavioral threats. This paper presents MQTT-HS, a proxy-mediated security protocol that combines certificate-based authentication, ephemeral ECDH/HKDF session establishment, AES-256-GCM payload protection, controlled key refresh, and metadata-based hierarchical intrusion detection with inline enforcement. ProVerif verified the modeled secrecy, authentication, replay-resistance, message-flow agreement, and epoch-key secrecy properties of the cryptographic core. MQTT-HS supports forward secrecy across expired epochs through fresh ephemeral ECDH material, independent epoch-key derivation, and secure erasure of obsolete key material. An ESP32 implementation delivered all 360 protected messages and completed six in-session rekeys, with an average AES-256-GCM encryption latency of 0.354 ms per message. Controlled runtime experiments rejected all evaluated replay, untrusted-certificate, and invalid-signature attempts. The hierarchical XGBoost IDS achieved balanced accuracies of 0.808, 0.960, and 0.862 across its three stages, although Stage 0 produced a 37.5% false-positive rate on the limited legitimate holdout subset. Compared with the evaluated mutual TLS baselines, MQTT-HS preserved more endpoint free heap and provided MQTT-aware detection and enforcement, while requiring greater network bandwidth and a trusted Security Proxy. The results support the feasibility of MQTT-HS under the evaluated prototype configuration.

Read PDF

Similar papers

Preprint Oct 2026

HPQ-AKE: A Provably Secure Sign-Less Hybrid Authenticated Key Exchange Protocol for Bandwidth-Constrained IoT and Edge Networks

Securing bandwidth-constrained Internet of Things (IoT) and edge networks during post-quantum migration creates an authentication trade-off: ML-KEM provides post-quantum key establishment, whereas post-quantum signatures increase certificate-chain size, verification cost, and handshake latency. We present HPQ-AKE, a si...

Khiem Pham-Tuan, Minh Quang Le, Khuong Nguyen-An · 0 citations
Open access Aug 2026

Blockchain-Assisted Authentication, Authorization, and Audit for MQTT-Based Smart-City IoT

This work evaluates blockchain and smart contracts as a complementary trust layer for MQTT-based smart-city IoT rather than as a replacement for transport-layer security, position blockchain as an audit and policy-enforcement component for MQTT-based IoT.

Rida Lkhluf, David Santo Orcero, F. J. Cañete · 0 citations
Open access Sep 2026

Hardware-assisted zero-knowledge authentication scheme for resource-constrained IoT terminals: USBKEY implementation and evaluation based on GSVOLE-2DLC

Protocol performance and functional tests indicate that the proposed scheme can correctly execute identity authentication under the assumed threat model, making it suitable for IoT edge scenarios requiring privacy protection and lightweight authentication.

Jian-Xin Wang, Zi-Fan Xu, Run-Ze Zhou et al. · 0 citations

Formal Verification of Quantum-Resilient Authentication and Handover Protocols for LDACS

A systematic security and vulnerability assessment of LDACS authentication and mobility mechanisms using formal symbolic verification with the Tamarin prover provides formal evidence that the analyzed security mechanisms effectively mitigate cyber risks and enhance operational resilience, thereby supporting the safety...

SulemanKhan, GurjotSinghGaba, AndreiGurtov · 0 citations
Sep 2026

Secure over-the-air firmware update mechanism for embedded IoT devices using lightweight cryptographic authentication

Securing over-the-air firmware updates for resource-constrained IoT devices remains challenging, as existing solutions either rely on memory-intensive cryptographic algorithms or provide only basic integrity checks. This study aims to address this gap by developing a resource-efficient yet cryptographically comprehensi...

Xiang-Ning Meng · 0 citations
Book Open access Nov 2026

Provably Secure Practical Lightweight Post-Quantum Key Establishment for IoMT

This paper introduces PQ-LiteKEM, a formally verified, lightweight post-quantum security protocol for energy- and resource-constrained Internet of Medical Things (IoMT) devices. Addressing near-term quantum threats and emerging regulatory mandates such as the EU Cyber Resilience Act, the protocol mitigates the ‘harvest...

J. Prasad, Pardeep Kumar, Martin Duffy et al. · 0 citations

We use cookies to run the site and, with your consent, for analytics and to show ads. See our Cookie Policy.