We present a security analysis for one of the most popular standards for the Internet of Things, namely the MQ Telemetry Transport (MQTT) protocol, based on a formal model of the protocol in a timed process algebra. We explain the modelling choices we made and give a review of the results of earlier work on the formal verification of the protocol model. We also reveal in this chapter new results related to another case of its message delivery semantics, namely that of at-least-once delivery. We discuss the implications of different failure scenarios for clients and servers in the protocol as well as the variations in the attacker models that could affect the security guarantees of the protocol.