Sperrvermerk: Towards Formal Methods of IoT Application Layer Protocols

Sperrvermerk: This paper provides an overview of the application of formal methods for two most commonly used application layer protocols in IoT domain, MQTT and CoAP. Formal methods give the possibility to improve security and are even able to provide security guarantees with respect to a given model. Our research shows, that we can distinguish three formal verification fields for the two protocols, namely qualitative and quantitative analysis, implementations and security properties. A formal verification review of selected protocols is provided in accordance with these fields, used tools and considered properties. Based on that research, a short summary and open challenges are given.