Towards a formal modelling, analysis and verification of a clone node attack detection scheme in the internet of things

A clone node attack is one of the severe attacks on the Internet of Things (IoT) network. In a clone node attack, an adversary aims to physically capture the secret credentials of the deployed IoT devices to make the clone of devices look similar to the original devices. In recent years, several solutions for detecting clone node attacks have been designed; however, the focus of such designed solutions is on system design discussion, specific feature sets, high-level abstraction of underlying system architecture and fulfilling the performance analysis requirements. While the designed solutions efficiently detect clone attacks, critical features such as modelling, analysis, and verification of such solutions are frequently overlooked, necessitating that users verify their internal behaviour and claimed properties to ensure that no problematic scenarios or anomalies exist. Taking into account the rationale for formal verification and the limitations of previous works, this paper aims to perform formal modelling, analysis, and verification of our existing proposed clone node attack detection scheme for IoT. We used the High-Level Petri Nets (HLPNs) and Z-specification language to model our proposed scheme and analyse the logic correctness of our scheme using incidence markings and confidence interval matrices. To validate the functional correctness, we utilised the Satisfiability Modulo Theories Library (SMT-Lib) and the Z3 Solver and verified the functional satisfiable properties by analysing sat/unsat verification results and their execution time. Finally, we extend our modelling work by utilising the Coloured Petri Nets (CPNs), taking into consideration their both timed and untimed models with the aim of validating functional correctness and logical correctness, respectively. To analyse both correctnesses of CPN models, we used logging facility statistics such as count, sum, average, minimum, and maximum as data packet observations.