  In a clone node attack, an attacker attempted to physically capture the
devices to gather sensitive information to conduct various insider attacks.
Several solutions for detecting clone node attacks on IoT networks have been
presented in the viewpoints above. These solutions are focused on specific
system designs, processes, and feature sets and act as a high-level abstraction
of underlying system architectures based on a few performance requirements.
However, critical features like formal analysis, modelling, and verification
are frequently overlooked in existing proposed solutions aimed at verifying the
correctness and robustness of systems in order to ensure that no problematic
scenarios or anomalies exist. This paper presents a formal analysis, modelling,
and verification of our existing proposed clone node attack detection scheme in
IoT. Firstly, we modelled the architectural components of the proposed scheme
using High-Level Petri Nets (HLPNs) and then mapped them using their specified
functionalities. Secondly, we defined and analysed the behavioural properties
of the proposed scheme using Z specification language. Furthermore, we used the
Satisfiability Modulo Theories Library (SMT-Lib) and the Z3 Solver to validate
and demonstrate the overall functionality of the proposed scheme. Finally, in
addition to modelling and analysis, this work employs Coloured Petri Nets
(CPNs), which combine Petri Nets with a high-level programming language, making
them more suitable for large-scale system modelling. To perform the simulations
in CPN, we used both timed and untimed models, where timed models are used to
evaluate performance, and untimed models are used to validate logical validity.
