The Model Checking D2D and Centralised IOT authentication Protocols.

Abstract

It is very difficult to develop a perfect security protocol for communication over the IoT network and developing a reliable authentication protocol requires a detailed understanding of cryptography. To ensure the reliability of security protocols of IoT, the validation method is not a good choice because of its several disadvantages and limitations. To prove the high reliability of Cryptographic Security Protocols(CSP) for IoT networks, the functional correctness of security protocols must be proved secure mathematically. Using the Formal Verification technique[4] we can prove the functional correctness of IoT security protocols by providing the proofs mathematically. In this work, The CoAP[1](constrained application protocol) and CHAP[2] Device-to-Device (D2D) authentication protocols and centralised IoT network Authentication Protocol SSH[3] (Secure Shell) used in smart city applications are formally verified using the well-known verification technique known as model checking technique and we have used the Scyther[5] model checker for the verification of security properties of the respective protocols. The abstract protocol models of the IoT authentication protocols were specified in the security protocol description language and the security requirements of the authentication protocols were specified as claim events.