doi:10.1007/s11416-022-00444-zengRaimondo, M.Bernardi, S.Marrone, S.Merseguer, J.An approach for the automatic verification of blockchain protocols: the Tweetchain case studyART-2023-131433This 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.2023http://zaguan.unizar.es/record/12092110.1007/s11416-022-00444-zhttp://zaguan.unizar.es/record/120921oai:zaguan.unizar.es:120921info:eu-repo/grantAgreement/ES/MICINN/PID2020-113969RB-I00Journal of computer virology and hacking techniques 19, 1 (2023), 17-32byhttp://creativecommons.org/licenses/by/3.0/es/info:eu-repo/semantics/openAccess