eCite Digital Repository

A formally verified blockchain-based decentralised authentication scheme for the internet of things


Hameed, K and Garg, S and Amin, MB and Kang, B, A formally verified blockchain-based decentralised authentication scheme for the internet of things, Journal of Supercomputing pp. 1-41. ISSN 0920-8542 (2021) [Refereed Article]

Copyright Statement

The Author(s), under exclusive licence to Springer Science+Business Media, LLC, part of Springer Nature 2021

DOI: doi:10.1007/s11227-021-03841-1


With the proliferation of intelligent devices in the Internet of Things (IoT), the security of IoT devices is becoming a major concern as an attacker can exploit network services via network capture or deployment of malicious devices. Therefore, IoT device authentication is a key security requirement. Conventional authentication approaches have proved insufficient in dealing with a large number of IoT devices because of various shortcomings, such as centrally designed architectures and expensive cryptographic primitives. Blockchain technology has led to the creation of decentralised IoT authentication solutions with their desirable characteristics. Due to the integration of IoT and Blockchain technology, however, performance is one of the significant challenges. Existing Blockchain-based authentication schemes create extra storage, computing and communication overheads on the Blockchain which restricts its use for different IoT networks. In this paper, we design an efficient decentralised Blockchain-based authentication scheme aimed at achieving a secure authentication for IoT devices using the token mechanism. We design the Ethereum Blockchain network model to implement our scheme, in which smart contracts provide secure connectivity between miner nodes and IoT devices. We demonstrate our proposed scheme with an IoT-based smart home case study, which shows significant performance in computation and communication overheads compared with existing Blockchain-based authentication schemes. The modelling, analysis and verification of the proposed scheme, using high level Petri nets (HLPNs) and Z3 SMT solver are also provided to prove correctness and to verify the claims of our model.

Item Details

Item Type:Refereed Article
Keywords:internet of things, blockchain, IoT device, authentication, security, formal modelling, verification
Research Division:Information and Computing Sciences
Research Group:Distributed computing and systems software
Research Field:Distributed systems and algorithms
Objective Division:Information and Communication Services
Objective Group:Communication technologies, systems and services
Objective Field:Communication technologies, systems and services not elsewhere classified
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:145959
Year Published:2021
Web of Science® Times Cited:6
Deposited By:Information and Communication Technology
Deposited On:2021-08-13
Last Modified:2022-04-27

Repository Staff Only: item control page