120921 20240731103310.0 doi 10.1007/s11416-022-00444-z sideral 131433 ART-2023-131433 eng Raimondo, M. An approach for the automatic verification of blockchain protocols: the Tweetchain case study 2023 Access copy available to the general public Unrestricted 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. info:eu-repo/grantAgreement/ES/MICINN/PID2020-113969RB-I00 info:eu-repo/semantics/openAccess by http://creativecommons.org/licenses/by/3.0/es/ 0.443 2023 Computer Science (miscellaneous) 2023 Q2 Software 2023 Q3 Hardware and Architecture 2023 Q3 Computational Theory and Mathematics 2023 Q3 4.0 2023 info:eu-repo/semantics/article info:eu-repo/semantics/publishedVersion Bernardi, S. Universidad de Zaragoza (orcid)0000-0002-2605-6243 Marrone, S. Merseguer, J. Universidad de Zaragoza (orcid)0000-0002-8917-6584 5007 570 Universidad de Zaragoza Dpto. Informát.Ingenie.Sistms. Área Lenguajes y Sistemas Inf. 19, 1 (2023), 17-32 J. comput. virol. hacking tech. Journal of computer virology and hacking techniques 2263-8733 1555018 http://zaguan.unizar.es/record/120921/files/texto_completo.pdf Versión publicada 2252130 http://zaguan.unizar.es/record/120921/files/texto_completo.jpg?subformat=icon icon Versión publicada oai:zaguan.unizar.es:120921 articulos driver 2024-07-31-09:39:16 ARTICLE