FVF-BIoT: a formal verification framework for blockchain-based IoT authentication

【Author】 Yin, Jiaqi; Fei, Yuan

【Source】SOFTWARE QUALITY JOURNAL

【影响因子】1.813

【Abstract】Traditional IoT authentication methods, often centralized and reliant on a Trusted Third Party (TTP), face issues like high communication costs and vulnerability to data loss. Blockchain-based Internet of Things (IoT) authentication can effectively solve the problems brought by traditional IoT authentication. Because the authentication schemes are usually deployed on a large number of IoT devices it would be extremely expensive when there are issues to be fixed after the authentication schemes is deployed. Performing verification early at design time can alleviate this problem. To focus on these requirements, this article proposes a formal verification framework for blockchain-based IoT authentication (FVF-BIoT). Specifically, we design data type mapping and the conversion of elements in smart contracts for the authentication. Then we formalize the smart contracts into formal models in the interactive theorem prover Coq. Several algorithms are presented for the conversion of the smart contracts and the generation of examples. Examples and security properties related to contracts are described in the form of theorems, which are also proved by Coq. Through a case study, we not only demonstrate the effectiveness of the FVF-BIoT framework in ensuring the security and reliability of blockchain technology for IoT authentication but also highlight its innovative integration of formal verification processes. This distinctly addresses the previously unmet need for rigorous, mathematically proven security validations in the design and deployment of blockchain-based IoT authentication methods.

【Keywords】Formal verification; Theorem proving; Blockchain; Smart contract; IoT authantication

【发表时间】2024 2024 JUL 20

【收录时间】2024-07-27

【文献类型】

【主题类别】

--