{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T21:21:32Z","timestamp":1740172892551,"version":"3.37.3"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,8,25]],"date-time":"2022-08-25T00:00:00Z","timestamp":1661385600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,25]],"date-time":"2022-08-25T00:00:00Z","timestamp":1661385600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100015562","name":"INPS","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100015562","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100014440","name":"Ministerio de Ciencia, Innovaci\u00f3n y Universidades","doi-asserted-by":"publisher","award":["PID2020-113969RB-I00","PID2020-113969RB-I00"],"award-info":[{"award-number":["PID2020-113969RB-I00","PID2020-113969RB-I00"]}],"id":[{"id":"10.13039\/100014440","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Comput Virol Hack Tech"],"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 &amp;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.<\/jats:p>","DOI":"10.1007\/s11416-022-00444-z","type":"journal-article","created":{"date-parts":[[2022,8,25]],"date-time":"2022-08-25T14:03:22Z","timestamp":1661436202000},"page":"17-32","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An approach for the automatic verification of blockchain protocols: the Tweetchain case study"],"prefix":"10.1007","volume":"19","author":[{"given":"Mariapia","family":"Raimondo","sequence":"first","affiliation":[]},{"given":"Simona","family":"Bernardi","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1927-6173","authenticated-orcid":false,"given":"Stefano","family":"Marrone","sequence":"additional","affiliation":[]},{"given":"Jos\u00e9","family":"Merseguer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,25]]},"reference":[{"key":"444_CR1","volume-title":"Blockchain in Action","author":"B Ramamurthy","year":"2020","unstructured":"Ramamurthy, B.: Blockchain in Action. Manning, Shelter Island (2020)"},{"key":"444_CR2","doi-asserted-by":"publisher","unstructured":"Yaga, D., Mell, P., Roby, N., Scarfone, K.: Blockchain Technology Overview. Technical report, National Institute of Standards and Technology (2018). https:\/\/doi.org\/10.6028\/NIST.IR.8202","DOI":"10.6028\/NIST.IR.8202"},{"key":"444_CR3","doi-asserted-by":"publisher","unstructured":"Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Symbolic Analysis of Security Protocols. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 8044 LNCS, pp. 696\u2013701 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_48","DOI":"10.1007\/978-3-642-39799-8_48"},{"key":"444_CR4","doi-asserted-by":"publisher","unstructured":"Boyd, C., Gj\u00f8steen, K., Wu, S.: A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract. In: Bernardo, B., Marmsoler, D. (eds.) 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, July 20-21, 2020, (Virtual Conference). OASIcs, vol. 84, pp. 5\u20131513. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Los Angeles (USA) (2020). https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2020.5","DOI":"10.4230\/OASIcs.FMBC.2020.5"},{"key":"444_CR5","doi-asserted-by":"publisher","unstructured":"Basin, D., Keller, M., Radomirovi\u0107, S., Sasse, R.: Alice and Bob Meet Equational Theories. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9200, pp. 160\u2013180 (2015). https:\/\/doi.org\/10.1007\/978-3-319-23165-5_7","DOI":"10.1007\/978-3-319-23165-5_7"},{"key":"444_CR6","doi-asserted-by":"publisher","unstructured":"M\u00f6dersheim, S.: Algebraic Properties in Alice and Bob Notation. In: Proceedings of the The Forth International Conference on Availability, Reliability and Security, ARES 2009, March 16\u201319, 2009, pp. 433\u2013440. IEEE Computer Society, Fukuoka (2009). https:\/\/doi.org\/10.1109\/ARES.2009.95","DOI":"10.1109\/ARES.2009.95"},{"key":"444_CR7","doi-asserted-by":"publisher","unstructured":"Buccafurri, F., Lax, G., Nicolazzo, S., Nocera, A.: Overcoming Limits of Blockchain for IoT Applications. In: ACM International Conference Proceeding Series, vol. Part F130521 (2017). https:\/\/doi.org\/10.1145\/3098954.3098983","DOI":"10.1145\/3098954.3098983"},{"key":"444_CR8","doi-asserted-by":"crossref","unstructured":"Raimondo, M., Bernardi, S., Marrone, S.: On formalising and analysing the Tweetchain protocol. In: ICISSP 2021\u2014Proceedings of the 7th International Conference on Information Systems Security and Privacy, pp. 781\u2013791 (2021)","DOI":"10.5220\/0010427907810791"},{"key":"444_CR9","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2019.101654","volume":"88","author":"A Singh","year":"2020","unstructured":"Singh, A., Parizi, R.M., Zhang, Q., Choo, K.-K.R., Dehghantanha, A.: Blockchain smart contracts formalization: approaches and challenges to address vulnerabilities. Comput. Secur. 88, 101654 (2020). https:\/\/doi.org\/10.1016\/j.cose.2019.101654","journal-title":"Comput. Secur."},{"key":"444_CR10","doi-asserted-by":"publisher","unstructured":"Duan, Z., Mao, H., Chen, Z., Bai, X., Hu, K., Talpin, J.P.: Formal modeling and verification of blockchain system. In: Proceedings of the 10th International Conference on Computer Modeling and Simulation. ICCMS 2018, pp. 231\u2013235. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3177457.3177485","DOI":"10.1145\/3177457.3177485"},{"key":"444_CR11","unstructured":"Egger, C., Graf, M., K\u00fcsters, R., Rausch, D., Ronge, V., Schr\u00f6der, D.: A Security Framework for Distributed Ledgers. IACR Cryptol. ePrint Arch., vol. 145 (2021)"},{"key":"444_CR12","doi-asserted-by":"publisher","unstructured":"Thin, W.Y.M., Dong, N., Bai, G., Dong, J.S.: Formal analysis of a proof-of-stake blockchain. In: 2018 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 197\u2013200 (2018). https:\/\/doi.org\/10.1109\/ICECCS2018.2018.00031","DOI":"10.1109\/ICECCS2018.2018.00031"},{"key":"444_CR13","unstructured":"Tolmach, P., Li, Y., Lin, S.-W., Liu, Y.: Formal Analysis of Composable DeFi Protocols. In: Bernhard, M., Bracciali, A., Gudgeon, L., Haines, T., Klages-Mundt, A., Matsuo, S., Perez, D., Sala, M., Werner, S. (eds.) Financial Cryptography and Data Security. FC 2021 International Workshops, pp. 149\u2013161. Springer, Berlin (2021)"},{"key":"444_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/j.cose.2021.102279","volume":"107","author":"P Modesti","year":"2021","unstructured":"Modesti, P., Shahandashti, S.F., McCorry, P., Hao, F.: Formal modelling and security analysis of Bitcoin\u2019s payment protocol. Comput. Secur. 107, 102279 (2021). https:\/\/doi.org\/10.1016\/j.cose.2021.102279","journal-title":"Comput. Secur."},{"key":"444_CR15","doi-asserted-by":"crossref","unstructured":"Camenisch, J., Krenn, S., K\u00fcsters, R., Rausch, D.: iUC: flexible universal composability made simple. In: Advances in Cryptology\u2014ASIACRYPT 2019\u201425th International Conference on the Theory and Application of Cryptology and Information Security, December 8\u201312, 2019, Proceedings, Part III. Lecture Notes in Computer Science, vol. 11923, pp. 191\u2013221. Springer, Kobe (2019)","DOI":"10.1007\/978-3-030-34618-8_7"},{"key":"444_CR16","doi-asserted-by":"publisher","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating Specification and Programs for System Modeling and Verification. In: 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 127\u2013135 (2009). https:\/\/doi.org\/10.1109\/TASE.2009.32","DOI":"10.1109\/TASE.2009.32"},{"key":"444_CR17","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, pp. 709\u2013714. Springer, Berlin (2009)"},{"issue":"3","key":"444_CR18","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/s10207-004-0055-7","volume":"4","author":"DA Basin","year":"2005","unstructured":"Basin, D.A., M\u00f6dersheim, S., Vigan\u00f2, L.: OFMC: a symbolic model checker for security protocols. Int. J. Inf. Secur. 4(3), 181\u2013208 (2005). https:\/\/doi.org\/10.1007\/s10207-004-0055-7","journal-title":"Int. J. Inf. Secur."},{"key":"444_CR19","doi-asserted-by":"publisher","DOI":"10.3390\/fi12120222","author":"L K\u00f6nig","year":"2020","unstructured":"K\u00f6nig, L., Korobeinikova, Y., Tjoa, S., Kieseberg, P.: Comparing blockchain standards and recommendations. Future Internet (2020). https:\/\/doi.org\/10.3390\/fi12120222","journal-title":"Future Internet"},{"key":"444_CR20","unstructured":"Blockchain Ecosystem Interoperability. Technical report, Object Management Group (2019). RFI: mars\/19-08-03"},{"key":"444_CR21","unstructured":"Ellervee, A., Matulevic\u0306ius, R., Mayer, N.: A comprehensive reference model for blockchain-based distributed ledger technology. In: ER Forum\/Demos (2017)"},{"key":"444_CR22","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/978-3-030-37933-9_10","volume-title":"Advances in Enterprise Engineering XIII","author":"M Skotnica","year":"2020","unstructured":"Skotnica, M., Pergl, R.: Das contract\u2014a visual domain specific language for modeling blockchain smart contracts. In: Aveiro, D., Guizzardi, G., Borbinha, J. (eds.) Advances in Enterprise Engineering XIII, pp. 149\u2013166. Springer, Cham (2020)"},{"key":"444_CR23","unstructured":"UML\n$$^{\\rm TM}$$ Profile for Modeling Quality of Service and Fault Tolerance Characteristics and Mechanisms Specification. Technical report, Object Management Group (2005). formal-08-04-05"},{"key":"444_CR24","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/3-540-45800-X_33","volume-title":"UML2002\u2014The Unified Modeling Language","author":"T Lodderstedt","year":"2002","unstructured":"Lodderstedt, T., Basin, D., Doser, J.: Secureuml: a UML-based modeling language for model-driven security. In: J\u00e9z\u00e9quel, J.-M., Hussmann, H., Cook, S. (eds.) UML2002\u2014The Unified Modeling Language, pp. 426\u2013441. Springer, Berlin (2002)"},{"key":"444_CR25","doi-asserted-by":"publisher","unstructured":"J\u00fcrjens, J.: Secure Systems Development with UML. Springer, Berlin (2005). https:\/\/doi.org\/10.1007\/b137706","DOI":"10.1007\/b137706"},{"issue":"10","key":"444_CR26","doi-asserted-by":"publisher","first-page":"2313","DOI":"10.1093\/comjnl\/bxu096","volume":"58","author":"RJ Rodr\u00edguez","year":"2015","unstructured":"Rodr\u00edguez, R.J., Merseguer, J., Bernardi, S.: Modelling security of critical infrastructures: a survivability assessment. Comput. J. 58(10), 2313\u20132327 (2015). https:\/\/doi.org\/10.1093\/comjnl\/bxu096","journal-title":"Comput. J."},{"issue":"5","key":"444_CR27","doi-asserted-by":"publisher","first-page":"815","DOI":"10.1016\/j.infsof.2008.05.011","volume":"51","author":"D Basin","year":"2009","unstructured":"Basin, D., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Inf. Softw. Technol. 51(5), 815\u2013831 (2009). https:\/\/doi.org\/10.1016\/j.infsof.2008.05.011","journal-title":"Inf. Softw. Technol."},{"key":"444_CR28","doi-asserted-by":"publisher","unstructured":"J\u00fcrjens, J., Fox, J.: Tools for model-based security engineering. In: Osterweil, L.J., Rombach, H.D., Soffa, M.L. (eds.) 28th International Conference on Software Engineering (ICSE 2006), May 20\u201328, 2006, pp. 819\u2013822. ACM, Shanghai (2006). https:\/\/doi.org\/10.1145\/1134285.1134423","DOI":"10.1145\/1134285.1134423"},{"key":"444_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"286","DOI":"10.1007\/3-540-47884-1_16","volume-title":"IFM","author":"S Kent","year":"2002","unstructured":"Kent, S.: Model driven engineering. In: Butler, M.J., Petre, L., Sere, K. (eds.) IFM. Lecture Notes in Computer Science, vol. 2335, pp. 286\u2013298. Springer, Berlin (2002)"},{"key":"444_CR30","unstructured":"Ivanov, I., B\u00e9zivin, J., Aksit, M.: Technological spaces: an initial appraisal. In: 4th International Symposium on Distributed Objects and Applications, DOA 2002\u2014University of California, Irvine, United States, pp. 1\u20136 (2002). https:\/\/research.utwente.nl\/en\/publications\/technological-spaces-an-initial-appraisal"},{"key":"444_CR31","doi-asserted-by":"crossref","unstructured":"B\u00e9zivin, J., Devedzic, V., Djuric, D., Favreau, J.-M., Gasevic, D., Jouault, F.: An m3-neutral infrastructure for bridging model engineering and ontology engineering. In: Konstantas, D., Bourri\u00e8res, J.-P., L\u00e9onard, M., Boudjlida, N. (eds.) Interoperability of Enterprise Software and Applications, pp. 159\u2013171. Springer, London (2006)","DOI":"10.1007\/1-84628-152-0_15"},{"key":"444_CR32","unstructured":"B\u00e9zivin, J., Kurtev, I.: Model-based Technology Integration with the Technical Space Concept. Metainformatics Symposium (2006). https:\/\/hal.archives-ouvertes.fr\/hal-00483587"},{"key":"444_CR33","unstructured":"PlantUML. https:\/\/plantuml.com\/en\/sequence-diagram. Accessed 11 July 2021"},{"key":"444_CR34","unstructured":"Web Sequence Diagrams. https:\/\/www.websequencediagrams.com\/. Accessed 11 July 2021"},{"key":"444_CR35","doi-asserted-by":"publisher","unstructured":"Cortellessa, V., Marco, A.D., Inverardi, P.: Model-Based Software Performance Analysis. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-13621-4","DOI":"10.1007\/978-3-642-13621-4"},{"key":"444_CR36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39512-3","volume-title":"Model-Driven Dependability Assessment of Software Systems","author":"S Bernardi","year":"2013","unstructured":"Bernardi, S., Merseguer, J., Petriu, D.C.: Model-Driven Dependability Assessment of Software Systems. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39512-3"},{"key":"444_CR37","doi-asserted-by":"publisher","unstructured":"Bernardi, S., Gentile, U., Marrone, S., Merseguer, J., Nardone, R.: Security modelling and formal verification of survivability properties: application to cyber-physical systems. J. Syst. Softw. 171, 110746 (2021). https:\/\/doi.org\/10.1016\/j.jss.2020.110746","DOI":"10.1016\/j.jss.2020.110746"},{"issue":"2","key":"444_CR38","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1109\/TIT.1983.1056650","volume":"29","author":"D Dolev","year":"1983","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198\u2013208 (1983). https:\/\/doi.org\/10.1109\/TIT.1983.1056650","journal-title":"IEEE Trans. Inf. Theory"},{"issue":"3","key":"444_CR39","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/s10270-009-0128-1","volume":"10","author":"S Bernardi","year":"2011","unstructured":"Bernardi, S., Merseguer, J., Petriu, D.C.: A dependability profile within MARTE. Softw. Syst. Model. 10(3), 313\u2013336 (2011). https:\/\/doi.org\/10.1007\/s10270-009-0128-1","journal-title":"Softw. Syst. Model."},{"key":"444_CR40","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1016\/j.ress.2013.06.032","volume":"120","author":"S Bernardi","year":"2013","unstructured":"Bernardi, S., Flammini, F., Marrone, S., Mazzocca, N., Merseguer, J., Nardone, R., Vittorini, V.: Enabling the usage of UML in the verification of railway systems: the dam-rail approach. Rel. Eng. Sys. Saf. 120, 112\u2013126 (2013). https:\/\/doi.org\/10.1016\/j.ress.2013.06.032","journal-title":"Rel. Eng. Sys. Saf."},{"key":"444_CR41","doi-asserted-by":"crossref","unstructured":"Selic, B.: A systematic approach to domain-specific language design using UML. In: 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC\u201907), pp. 2\u20139 (2007)","DOI":"10.1109\/ISORC.2007.10"},{"key":"444_CR42","doi-asserted-by":"crossref","unstructured":"Lagarde, F., et al.: Improving UML profile design practices by leveraging conceptual domain models. In: 22nd International Conference on Automated Software Engineering, pp. 445\u2013448. ACM, Atlanta (2007)","DOI":"10.1145\/1321631.1321705"},{"key":"444_CR43","doi-asserted-by":"publisher","unstructured":"Buccafurri, F., Lax, G., Nicolazzo, S., Nocera, A.: Tweetchain: an alternative to blockchain for crowd-based applications. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 10360 LNCS, pp. 386\u2013393 (2017). https:\/\/doi.org\/10.1007\/978-3-319-60131-1_24","DOI":"10.1007\/978-3-319-60131-1_24"},{"key":"444_CR44","unstructured":"Keller, M.: Converting Alice &Bob Protocol Specifications to Tamarin. Bachelor\u2019s Thesis, Swiss Federal Institute of Technology Zurich (2014)"},{"key":"444_CR45","unstructured":"OMG: Unified Modelling Language: Superstructure. Object Management Group (2015). Object Management Group. Version 2.5, formal\/15-03-01"},{"key":"444_CR46","doi-asserted-by":"publisher","unstructured":"Cortier, V., Delaune, S., Dreier, J.: Automatic generation of sources lemmas in Tamarin: towards automatic proofs of security protocols. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 12309 LNCS, pp. 3\u201322 (2020). https:\/\/doi.org\/10.1007\/978-3-030-59013-0_1","DOI":"10.1007\/978-3-030-59013-0_1"}],"container-title":["Journal of Computer Virology and Hacking Techniques"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11416-022-00444-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11416-022-00444-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11416-022-00444-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,3,26]],"date-time":"2023-03-26T21:32:39Z","timestamp":1679866359000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11416-022-00444-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,8,25]]},"references-count":46,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2023,3]]}},"alternative-id":["444"],"URL":"https:\/\/doi.org\/10.1007\/s11416-022-00444-z","relation":{},"ISSN":["2263-8733"],"issn-type":[{"type":"electronic","value":"2263-8733"}],"subject":[],"published":{"date-parts":[[2022,8,25]]},"assertion":[{"value":"14 November 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 June 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 August 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}