Formal Specification and Verification of COAP Protocol Using Pluscal-2.

Abstract

Usage of internet is becoming more and more important in all aspects of life and with this rise the use of IoT based applications are growing very fast in recent times. IoT is transforming the industries and businesses like manufacturing, health system and communications network. Communication protocols are the core part of IoT and one such protocol is Constrained Application Protocol (CoAP). Just like most of the protocols poses large number of security vulnerabilities CoAP does not provide protocol security measures by itself, which makes it vulnerable to threats. In this paper, we respond to the need of formally verifying the CoAP. With Formal methods there is possibility in security improvements and measures. Our proposed formal model is based on the TLA+ and PlusCal-2, which will check the correctness properties of CoAP protocol and will also give the system’s execution trace in the event of failure. Our model is described in complete detail and its performance based results explains the practicability of this technique