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

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.