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

Raimondo, M. ; Bernardi, S. (Universidad de Zaragoza) ; Marrone, S. ; Merseguer, J. (Universidad de Zaragoza)

Resumen: 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.

Idioma: Inglés

DOI: 10.1007/s11416-022-00444-z

Año: 2023

Publicado en: Journal of computer virology and hacking techniques 19, 1 (2023), 17-32
ISSN: 2263-8733

Factor impacto SCIMAGO: 0.443 - Computer Science (miscellaneous) (Q2) - Software (Q3) - Hardware and Architecture (Q3) - Computational Theory and Mathematics (Q3)

Financiación: info:eu-repo/grantAgreement/ES/MICINN/PID2020-113969RB-I00

Tipo y forma: Artículo (Versión definitiva)

Área (Departamento): Área Lenguajes y Sistemas Inf. (Dpto. Informát.Ingenie.Sistms.)