An approach for the automatic verification of blockchain protocols: the Tweetchain case study
JOURNAL OF COMPUTER VIROLOGY AND HACKING TECHNIQUES(2022)
摘要
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.
更多查看译文
关键词
Distributed ledger technology, Formal modelling, Automatic model generation, Vulnerability discovery, Formal verification, UML profile
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要