Open AccessModel Checking M2M and Centralised IOT authentication Protocols.
Author(s) -
H. Swapna Rekha,
M. Siddappa
Publication year - 2022
Publication title -
journal of physics. conference series
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.21
H-Index - 85
eISSN - 1742-6596
pISSN - 1742-6588
DOI - 10.1088/1742-6596/2161/1/012042
Subject(s) - computer science , authentication protocol , correctness , cryptographic protocol , authentication (law) , otway–rees protocol , protocol (science) , hash based message authentication code , wide mouth frog protocol , computer security , challenge handshake authentication protocol , cryptography , reliability (semiconductor) , computer network , universal composability , formal verification , message authentication code , theoretical computer science , algorithm , medicine , power (physics) , physics , alternative medicine , pathology , quantum mechanics
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 we can prove the functional correctness of IoT security protocols by providing the proofs mathematically. In this work, The CoAP Machine to Machine authentication protocol and centralied IoT network Authentication Protocol RADIUS is formally verified using the well-known verification technique known as model checking technique and we have used the Scyther 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.