{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T23:26:46Z","timestamp":1766446006393,"version":"3.48.0"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2025,12,1]],"date-time":"2025-12-01T00:00:00Z","timestamp":1764547200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,12,20]],"date-time":"2025-12-20T00:00:00Z","timestamp":1766188800000},"content-version":"vor","delay-in-days":19,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100002835","name":"Chalmers University of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002835","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Discrete Event Dyn Syst"],"published-print":{"date-parts":[[2025,12]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Smart contracts are programs that can enforce agreements between mutually distrusting parties, eliminating the need for intermediaries, such as lawyers or banks. As smart contracts are stored on a blockchain ledger, they are immutable after deployment, which makes assessment of their correctness before deployment vital. Many vulnerabilities of smart contracts are known, and having means to assess whether a contract is prone to one or more of these is crucial. A specific such vulnerability is\n                    <jats:italic>denial-of-service<\/jats:italic>\n                    (DoS), which can make a smart contract unresponsive so that users (including other smart contracts) cannot interact with it as intended. This can lead (and has led) lead to financial losses, or disrupt critical services that rely on the contract. Extended finite state machines (EFSM) are a modelling formalism for discrete-event systems, which provides a systematic approach to scrutinize smart contract functionalities. With careful modeling, non-blocking verification can be used to determine whether a contract is vulnerable to DoS attacks. This paper describes a methodology to automatically convert from the abstract syntax tree of a smart contract to an EFSM model, and then shows how non-blocking verification can indeed assess whether DoS attacks can cause harm. Two specific use cases are treated, a contract implementing a (simple) on-line casino, and an auction contract. Verification of the EFSM models reveals both contracts to be prone to DoS attacks, and counterexamples hint at how the contracts can be made non-blocking, meaning that they can be corrected not to be vulnerable. Automatic conversion and non-blocking verification of the corrected contracts indeed show that they are no longer prone to DoS attacks.\n                  <\/jats:p>","DOI":"10.1007\/s10626-025-00418-5","type":"journal-article","created":{"date-parts":[[2025,12,19]],"date-time":"2025-12-19T23:57:46Z","timestamp":1766188666000},"page":"355-387","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Smart contract denial-of-service analysis using non-blocking verification"],"prefix":"10.1007","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-1994-2903","authenticated-orcid":false,"given":"Nishant","family":"Parekh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5671-2555","authenticated-orcid":false,"given":"Wolfgang","family":"Ahrendt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1287-9748","authenticated-orcid":false,"given":"Martin","family":"Fabian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,12,20]]},"reference":[{"key":"418_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt W, Bubel R (2020) Functional verification of smart contracts via strong data integrity. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation: applications. Springer International Publishing, Cham, pp 9\u201324. https:\/\/doi.org\/10.1007\/978-3-030-61467-6_2","DOI":"10.1007\/978-3-030-61467-6_2"},{"key":"418_CR2","doi-asserted-by":"publisher","unstructured":"Akesson K, Fabian M, Flordal H et\u00a0al (2006) Supremica \u2013 an integrated environment for verification, synthesis and simulation of discrete event systems. In: 2006 8th international workshop on discrete event systems. IEEE, pp 384\u2013385. https:\/\/doi.org\/10.1109\/WODES.2006.382401","DOI":"10.1109\/WODES.2006.382401"},{"key":"418_CR3","doi-asserted-by":"publisher","unstructured":"Atzei N, Bartoletti M, Cimoli T (2017) A survey of attacks on Ethereum smart contracts (SoK). In: Maffei M, Ryan M (eds) Principles of security and trust. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 164\u2013186. https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"418_CR4","doi-asserted-by":"publisher","unstructured":"Bai X, Cheng Z, Duan Z et\u00a0al (2018) Formal modeling and verification of smart contracts. In: Proceedings of the 2018 7th international conference on software and computer applications. Association for Computing Machinery, New York, NY, USA, ICSCA \u201918, pp 322\u2013326. https:\/\/doi.org\/10.1145\/3185089.3185138","DOI":"10.1145\/3185089.3185138"},{"key":"418_CR5","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen JP (2008) Principles of model checking. MIT Press"},{"key":"418_CR6","doi-asserted-by":"publisher","unstructured":"Barbosa H, Barrett C, Brain M et\u00a0al (2022) cvc5: a versatile and industrial-strength SMT solver. In: Fisman D, Rosu G (eds) Tools and algorithms for the construction and analysis of systems. Springer International Publishing, Cham, pp 415\u2013442. https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"418_CR7","doi-asserted-by":"publisher","unstructured":"Barrett C, Sebastiani R, Seshia SA et\u00a0al (2009) Satisfiability modulo theories. In: Handbook of satisfiability, frontiers in artificial intelligence and applications, vol 185. IOS Press, pp 825\u2013885. https:\/\/doi.org\/10.3233\/978-1-58603-929-5-825, https:\/\/ebooks.iospress.nl\/publication\/5011","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"418_CR8","doi-asserted-by":"publisher","unstructured":"Bartoletti M, Ferrando A, Lipparini E et\u00a0al (2024) Solvent: liquidity verification of smart contracts. In: Kosmatov N, Kov\u00e1cs L (eds) Integrated formal methods. Springer Nature Switzerland, Cham, pp 256\u2013266. https:\/\/doi.org\/10.1007\/978-3-031-76554-4_14","DOI":"10.1007\/978-3-031-76554-4_14"},{"key":"418_CR9","doi-asserted-by":"publisher","unstructured":"Cavada R, Cimatti A, Dorigatti M et\u00a0al (2014) The nuXmv symbolic model checker. In: Biere A, Bloem R (eds) Computer aided verification. Springer International Publishing, Cham, pp 334\u2013342. https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"418_CR10","doi-asserted-by":"publisher","unstructured":"Chen YL, Lin F (2000) Modeling of discrete event systems using finite state machines with parameters. In: Proceedings of the 2000. IEEE international conference on control applications. Conference Proceedings (Cat. No.00CH37162), pp 941\u2013946. https:\/\/doi.org\/10.1109\/CCA.2000.897591","DOI":"10.1109\/CCA.2000.897591"},{"key":"418_CR11","doi-asserted-by":"publisher","unstructured":"Cheng KT, Krishnakumar AS (1993) Automatic functional test generation using the extended finite state machine model. In: Proceedings of the 30th ACM\/IEEE design automation conference, pp 86\u201391. https:\/\/doi.org\/10.1145\/157485.164585","DOI":"10.1145\/157485.164585"},{"issue":"1","key":"418_CR12","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/225871.225880","volume":"1","author":"KT Cheng","year":"1996","unstructured":"Cheng KT, Krishnakumar AS (1996) Automatic generation of functional vectors using the extended finite state machine model. ACM Trans Des Autom Electron Syst 1(1):57\u201379. https:\/\/doi.org\/10.1145\/225871.225880","journal-title":"ACM Trans Des Autom Electron Syst"},{"key":"418_CR13","unstructured":"CoinGeek (2020) Over $$\\$1$$ million permanently locked in DeFi smart contract. https:\/\/coingeek.com\/over-1-million-permanently-locked-in-defi-smart-contract\/. Accessed 19 Nov 2024"},{"key":"418_CR14","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"418_CR15","doi-asserted-by":"publisher","unstructured":"Fekih R, Lahami M, Jmaiel M et\u00a0al (2022) Towards model checking approach for smart contract validation in the EIP-1559 Ethereum. In: 46th IEEE annual computers, software, and applications conference, COMPSAC 2022, Los Alamitos, CA, USA, June 27 - July 1, 2022, pp 83\u201388. https:\/\/doi.org\/10.1109\/COMPSAC54236.2022.00020","DOI":"10.1109\/COMPSAC54236.2022.00020"},{"key":"418_CR16","doi-asserted-by":"publisher","unstructured":"Godoy J, Galeotti JP, Garbervetsky D et\u00a0al (2022) Predicate abstractions for smart contract validation. In: Proceedings of the 25th international conference on model driven engineering languages and systems. association for computing machinery, New York, NY, USA, MODELS \u201922, pp 289\u2013299. https:\/\/doi.org\/10.1145\/3550355.3552462","DOI":"10.1145\/3550355.3552462"},{"key":"418_CR17","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice Hall"},{"issue":"5","key":"418_CR18","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G Holzmann","year":"1997","unstructured":"Holzmann G (1997) The model checker SPIN. IEEE Trans Software Eng 23(5):279\u2013295. https:\/\/doi.org\/10.1109\/32.588521","journal-title":"IEEE Trans Software Eng"},{"key":"418_CR19","unstructured":"ISO\/IEC\u00a021778 (2017) Information technology \u2013 the JSON data interchange syntax. https:\/\/www.iso.org\/standard\/71616.html. Accessed 23 Nov 2024"},{"key":"418_CR20","unstructured":"Konstantopoulos G (2018) How to secure your smart contracts: 6 solidity vulnerabilities and how to avoid them (part 2). https:\/\/medium.com\/loom-network\/how-to-secure-your-smart-contracts-6-so lidity-vulnerabilities-and-how-to-avoid-them-part-2-730db0aa4834. Accessed 24 Nov 2024"},{"key":"418_CR21","doi-asserted-by":"publisher","unstructured":"Madl G, Bathen L, Flores G et\u00a0al (2019) Formal verification of smart contracts using interface automata. In: 2019 IEEE international conference on blockchain (Blockchain), pp 556\u2013563. https:\/\/doi.org\/10.1109\/Blockchain.2019.00081","DOI":"10.1109\/Blockchain.2019.00081"},{"issue":"3","key":"418_CR22","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/s10626-023-00378-8","volume":"33","author":"R Malik","year":"2023","unstructured":"Malik R, Mohajerani S, Fabian M (2023) A survey on compositional algorithms for verification and synthesis in supervisory control. J Discrete Event Dyn Syst 33(3):279\u2013340. https:\/\/doi.org\/10.1007\/s10626-023-00378-8","journal-title":"J Discrete Event Dyn Syst"},{"issue":"4","key":"418_CR23","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s10626-022-00369-1","volume":"32","author":"S Matsui","year":"2022","unstructured":"Matsui S, Lafortune S (2022) Synthesis of winning attacks on communication protocols using supervisory control theory: two case studies. Discrete Event Dyn Syst 32(4):573\u2013610. https:\/\/doi.org\/10.1007\/s10626-022-00369-1","journal-title":"Discrete Event Dyn Syst"},{"key":"418_CR24","doi-asserted-by":"publisher","unstructured":"Mavridou A, Laszka A (2018) Designing secure Ethereum smart contracts: a finite state machine based approach. In: Meiklejohn S, Sako K (eds) Financial cryptography and data security. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 523\u2013540. https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28","DOI":"10.1007\/978-3-662-58387-6_28"},{"issue":"1","key":"418_CR25","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/s10626-015-0217-y","volume":"26","author":"S Mohajerani","year":"2016","unstructured":"Mohajerani S, Malik R, Fabian M (2016) A framework for compositional nonblocking verification of extended finite-state machines. J Discrete Event Dyn Syst 26(1):33\u201384. https:\/\/doi.org\/10.1007\/s10626-015-0217-y","journal-title":"J Discrete Event Dyn Syst"},{"key":"418_CR26","doi-asserted-by":"publisher","unstructured":"Mohajerani S, Ahrendt W, Fabian M (2022) Modeling and security verification of state-based smart contracts. IFAC-PapersOnLine 55(28):356\u2013362. https:\/\/doi.org\/10.1016\/j.ifacol.2022.10.366, 16th IFAC Workshop on Discrete Event Systems WODES 2022","DOI":"10.1016\/j.ifacol.2022.10.366"},{"key":"418_CR27","unstructured":"Mohajerani S, Malik R, Fabian M (2013) Partial unfolding for compositional nonblocking verification of extended finite-state machines. Tech. rep., Chalmers University of Technology, G\u00f6teborg, Sweden; also The University of Waikato, Hamilton, New Zealand. https:\/\/hdl.handle.net\/10289\/7140, https:\/\/research.chalmers.se\/publication\/172205"},{"key":"418_CR28","doi-asserted-by":"publisher","unstructured":"Parekh N, Ahrendt W, Fabian M (2024) Automatic conversion of smart contracts for non-blocking verification. IFAC-PapersOnLine 58(1):282\u2013287. https:\/\/doi.org\/10.1016\/j.ifacol.2024.07.048, 17th IFAC Workshop on Discrete Event Systems WODES 2024","DOI":"10.1016\/j.ifacol.2024.07.048"},{"key":"418_CR29","doi-asserted-by":"publisher","unstructured":"Parizi RM, Amritraj, Dehghantanha A (2018) Smart contract programming languages on blockchains: an empirical evaluation of usability and security. In: Chen S, Wang H, Zhang LJ (eds) Blockchain \u2013 ICBC 2018. Springer International Publishing, Cham, pp 75\u201391. https:\/\/doi.org\/10.1007\/978-3-319-94478-4_6","DOI":"10.1007\/978-3-319-94478-4_6"},{"issue":"1","key":"418_CR30","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"PJG Ramadge","year":"1989","unstructured":"Ramadge PJG, Wonham WM (1989) The control of discrete event systems. Proc IEEE 77(1):81\u201398","journal-title":"Proc IEEE"},{"key":"418_CR31","doi-asserted-by":"publisher","unstructured":"Richter Vidal F, Ivaki N, Laranjeiro N (2024) OpenSCV: an open hierarchical taxonomy for smart contract vulnerabilities. Empir Softw Eng 29. https:\/\/doi.org\/10.1007\/s10664-024-10446-8","DOI":"10.1007\/s10664-024-10446-8"},{"key":"418_CR32","doi-asserted-by":"publisher","unstructured":"Skoldstam M, Akesson K, Fabian M (2007) Modeling of discrete event systems using finite automata with variables. In: 2007 46th IEEE conference on decision and control, pp 3387\u20133392. https:\/\/doi.org\/10.1109\/CDC.2007.4434894","DOI":"10.1109\/CDC.2007.4434894"},{"key":"418_CR33","unstructured":"Suvorov D, Ulyantsev V (2019) Smart contract design meets state machine synthesis: case studies. arXiv:1906.02906"},{"key":"418_CR34","unstructured":"SWC\u00a0Registry (2020) Smart contract weakness classification (SWC). https:\/\/swcregistry.io\/docs\/SWC-113\/. Accessed 21 Nov 2024"},{"key":"418_CR35","unstructured":"VerifyThis (2021) VerifyThis long-term challenge. https:\/\/verifythis.github.io\/ltc\/02casino\/. Accessed 21 Nov 2024"},{"key":"418_CR36","unstructured":"Wikipedia (2024) Abstract syntax tree. https:\/\/en.wikipedia.org\/wiki\/Abstract_syntax_tree. Accessed 23 Nov 2024"},{"key":"418_CR37","unstructured":"Wood G (2023) Ethereum: a secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper. https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf"}],"container-title":["Discrete Event Dynamic Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-025-00418-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10626-025-00418-5","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10626-025-00418-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T23:22:10Z","timestamp":1766445730000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10626-025-00418-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,12]]},"references-count":37,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["418"],"URL":"https:\/\/doi.org\/10.1007\/s10626-025-00418-5","relation":{},"ISSN":["0924-6703","1573-7594"],"issn-type":[{"type":"print","value":"0924-6703"},{"type":"electronic","value":"1573-7594"}],"subject":[],"published":{"date-parts":[[2025,12]]},"assertion":[{"value":"10 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 December 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}]}}