eCite Digital Repository

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


Hameed, K and Garg, S and Amin, MB and Kang, B, Towards a formal modelling, analysis and verification of a clone node attack detection scheme in the internet of things, Computer Networks, 204 Article 108702. ISSN 1389-1286 (2022) [Refereed Article]

Copyright Statement

Copyright 2022 Elsevier B.V.

DOI: doi:10.1016/j.comnet.2021.108702


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.

Item Details

Item Type:Refereed Article
Keywords:Internet of Things, formal modelling, verification, validation, high level petri nets, coloured petri nets, networks security, IoT
Research Division:Information and Computing Sciences
Research Group:Distributed computing and systems software
Research Field:Cyberphysical systems and internet of things
Objective Division:Information and Communication Services
Objective Group:Information systems, technologies and services
Objective Field:Computer systems
UTAS Author:Hameed, K (Mr Hameed Khizar)
UTAS Author:Garg, S (Dr Saurabh Garg)
UTAS Author:Amin, MB (Dr Muhammad Bilal Amin)
UTAS Author:Kang, B (Professor Byeong Kang)
ID Code:148543
Year Published:2022
Deposited By:Information and Communication Technology
Deposited On:2022-01-21
Last Modified:2023-01-06

Repository Staff Only: item control page