000120921 001__ 120921
000120921 005__ 20240705134136.0
000120921 0247_ $$2doi$$a10.1007/s11416-022-00444-z
000120921 0248_ $$2sideral$$a131433
000120921 037__ $$aART-2023-131433
000120921 041__ $$aeng
000120921 100__ $$aRaimondo, M.
000120921 245__ $$aAn approach for the automatic verification of blockchain protocols: the Tweetchain case study
000120921 260__ $$c2023
000120921 5060_ $$aAccess copy available to the general public$$fUnrestricted
000120921 5203_ $$aThis 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.
000120921 536__ $$9info:eu-repo/grantAgreement/ES/MICINN/PID2020-113969RB-I00
000120921 540__ $$9info:eu-repo/semantics/openAccess$$aby$$uhttp://creativecommons.org/licenses/by/3.0/es/
000120921 592__ $$a0.443$$b2023
000120921 593__ $$aComputer Science (miscellaneous)$$c2023$$dQ2
000120921 593__ $$aSoftware$$c2023$$dQ3
000120921 593__ $$aHardware and Architecture$$c2023$$dQ3
000120921 593__ $$aComputational Theory and Mathematics$$c2023$$dQ3
000120921 655_4 $$ainfo:eu-repo/semantics/article$$vinfo:eu-repo/semantics/publishedVersion
000120921 700__ $$0(orcid)0000-0002-2605-6243$$aBernardi, S.$$uUniversidad de Zaragoza
000120921 700__ $$aMarrone, S.
000120921 700__ $$0(orcid)0000-0002-8917-6584$$aMerseguer, J.$$uUniversidad de Zaragoza
000120921 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf.
000120921 773__ $$g19, 1 (2023), 17-32$$pJ. comput. virol. hacking tech.$$tJournal of computer virology and hacking techniques$$x2263-8733
000120921 8564_ $$s1555018$$uhttps://zaguan.unizar.es/record/120921/files/texto_completo.pdf$$yVersión publicada
000120921 8564_ $$s2252130$$uhttps://zaguan.unizar.es/record/120921/files/texto_completo.jpg?subformat=icon$$xicon$$yVersión publicada
000120921 909CO $$ooai:zaguan.unizar.es:120921$$particulos$$pdriver
000120921 951__ $$a2024-07-05-12:45:47
000120921 980__ $$aARTICLE