000126389 001__ 126389 000126389 005__ 20230621161008.0 000126389 0247_ $$2doi$$a10.5220/0010427907810791 000126389 0248_ $$2sideral$$a124218 000126389 037__ $$aART-2021-124218 000126389 041__ $$aeng 000126389 100__ $$aRaimondo, M. 000126389 245__ $$aOn formalising and analysing the tweetchain protocol 000126389 260__ $$c2021 000126389 5060_ $$aAccess copy available to the general public$$fUnrestricted 000126389 5203_ $$aDistributed Ledger Technology is demonstrating its capability to provide flexible frameworks for information assurance capable of resisting to byzantine failures and multiple target attacks. The availability of development frameworks allows the definition of many applications using such a technology. On the contrary, the verification of such applications are far from being easy since testing is not enough to guarantee the absence of security problems. The paper describes an experience in the modelling and security analysis of one of these applications by means of formal methods: in particular, we consider the Tweetchain protocol as a case study and we use the Tamarin Prover tool, which supports the modelling of a protocol as a multiset rewriting system and its analysis with respect to temporal first-order properties. With the aim of making the modeling and verification process reproducible and independent of the specific protocol, we present a general structure of the Tamarin Prover model and of the properties to verified. Finally, we discuss the strengths and limitations of the Tamarin Prover approach considering three aspects: modelling, analysis and the verification process. Copyright 000126389 540__ $$9info:eu-repo/semantics/openAccess$$aby-nc-nd$$uhttp://creativecommons.org/licenses/by-nc-nd/3.0/es/ 000126389 655_4 $$ainfo:eu-repo/semantics/conferenceObject$$vinfo:eu-repo/semantics/publishedVersion 000126389 700__ $$0(orcid)0000-0002-2605-6243$$aBernardi, S.$$uUniversidad de Zaragoza 000126389 700__ $$aMarrone, S. 000126389 7102_ $$15007$$2570$$aUniversidad de Zaragoza$$bDpto. Informát.Ingenie.Sistms.$$cÁrea Lenguajes y Sistemas Inf. 000126389 773__ $$g1 (2021), 781-791$$pICISSP$$tICISSP$$x2184-3554 000126389 8564_ $$s887712$$uhttps://zaguan.unizar.es/record/126389/files/texto_completo.pdf$$yVersión publicada 000126389 8564_ $$s2478028$$uhttps://zaguan.unizar.es/record/126389/files/texto_completo.jpg?subformat=icon$$xicon$$yVersión publicada 000126389 909CO $$ooai:zaguan.unizar.es:126389$$particulos$$pdriver 000126389 951__ $$a2023-06-21-14:49:11 000126389 980__ $$aARTICLE