Formal verification for a PMQTT protocol

Abstract

The future of Internet of Things (IoT) foresees a world of interconnected people with every physical object in a seamless manner. The security related aspects for the IoT world are still an open field of discussion and research. The Message Queue Telemetry Transport (MQTT) application layer protocol is widely used in IoT networks. Since, MQTT standard has no mandatory requirements regarding the security services, therefore, manipulating the security related issues is different in MQTT platforms. This paper proposes a novel security protocol. It is the Protected Message Queue Telemetry Transport (PMQTT) protocol which is based on MQTT with added cryptographic primitives to offer security services for IoT systems. Moreover, a formal verification for a PMQTT protocol is conducted using the ProVerif cryptographic automated verifier tool to prove that the PMQTT protocol satisfies the intended security properties.

Keywords

• IoT
• MQTT
• Elliptic Curve Digital Signature Algorithm
• Elliptic Curve Diffie Hellman
• Formal verification
• ProVerif