A formal model and analysis of an IoT protocol
- Submitting institution
-
University of Portsmouth
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 7151294
- Type
- D - Journal article
- DOI
-
10.1016/j.adhoc.2015.05.013
- Title of journal
- Ad Hoc Networks
- Article number
- -
- First page
- 49
- Volume
- 36
- Issue
- 1
- ISSN
- 1570-8705
- Open access status
- Out of scope for open access requirements
- Month of publication
- January
- Year of publication
- 2016
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
0
- Research group(s)
-
C - Cyber Security
- Citation count
- 18
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- The paper represents a successful case study in the application of a robust and rigorous formal verification technique to a model of a complex IoT protocol (MQTT) widely used in networked systems and applications. The paper uncovered a serious flaw resulting in incorrect, and possibly insecure, behaviour in any device using MQTT. The paper was subsequently noted by the OASIS MQTT Technical Committee leading to changes in the MQTT standard, impacting and securing millions of existing devices already deployed and any MQTT deployments since 2015 (https://issues.oasis-open.org/browse/MQTT-209).
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -