An approach for the automatic verification of blockchain protocols: the Tweetchain case study

【Author】 Raimondo, Mariapia; Bernardi, Simona; Marrone, Stefano; Merseguer, Jose

【Source】JOURNAL OF COMPUTER VIROLOGY AND HACKING TECHNIQUES

【影响因子】0.000

【Abstract】This paper proposes a model-driven approach for the security modelling and analysis of blockchain based protocols. The modelling is built upon the definition of a UML profile, which is able to capture transaction-oriented information. The analysis is based on existing formal analysis tools. In particular, the paper considers the Tweetchain protocol, a recent proposal that leverages online social networks, i.e., Twitter, for extending blockchain to domains with small-value transactions, such as IoT. A specialized textual notation is added to the UML profile to capture features of this protocol. Furthermore, a model transformation is defined to generate a Tamarin model, from the UML models, via an intermediate well-known notation, i.e., the Alice &Bob notation. Finally, Tamarin Prover is used to verify the model of the protocol against some security properties. This work extends a previous one, where the Tamarin formal models were generated by hand. A comparison on the analysis results, both under the functional and non-functional aspects, is reported here too.

【Keywords】Distributed ledger technology; Formal modelling; Automatic model generation; Vulnerability discovery; Formal verification; UML profile

【发表时间】

【收录时间】2022-09-06

【文献类型】实验仿真

【主题类别】

区块链技术-核心技术-共识机制