{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T22:53:17Z","timestamp":1770331997059,"version":"3.49.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171377","type":"print"},{"value":"9783030171384","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17138-4_10","type":"book-chapter","created":{"date-parts":[[2019,4,2]],"date-time":"2019-04-02T14:04:43Z","timestamp":1554213883000},"page":"222-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["Verifying Liquidity of Bitcoin Contracts"],"prefix":"10.1007","author":[{"given":"Massimo","family":"Bartoletti","sequence":"first","affiliation":[]},{"given":"Roberto","family":"Zunino","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"key":"10_CR1","unstructured":"Understanding the DAO attack, June 2016. \n                    http:\/\/www.coindesk.com\/understanding-dao-hack-journalists\/"},{"key":"10_CR2","unstructured":"Parity Wallet security alert, July 2017. \n                    https:\/\/paritytech.io\/blog\/security-alert.html"},{"key":"10_CR3","unstructured":"A Postmortem on the Parity Multi-Sig library self-destruct, November 2017. \n                    https:\/\/goo.gl\/Kw3gXi"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-662-44774-1_8","volume-title":"Financial Cryptography and Data Security","author":"M Andrychowicz","year":"2014","unstructured":"Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, \u0141.: Fair two-party computations via Bitcoin deposits. In: B\u00f6hme, R., Brenner, M., Moore, T., Smith, M. (eds.) FC 2014. LNCS, vol. 8438, pp. 105\u2013121. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-662-44774-1_8"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-319-10512-3_2","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M Andrychowicz","year":"2014","unstructured":"Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, \u0141.: Modeling Bitcoin contracts by timed automata. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711, pp. 7\u201322. Springer, Cham (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-319-10512-3_2"},{"key":"10_CR6","unstructured":"Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Secure multiparty computations on Bitcoin. In: IEEE S & P, pp. 443\u2013458 (2014). First appeared on Cryptology ePrint Archive. \n                    http:\/\/eprint.iacr.org\/2013\/784"},{"issue":"4","key":"10_CR7","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/2896386","volume":"59","author":"M Andrychowicz","year":"2016","unstructured":"Andrychowicz, M., Dziembowski, S., Malinowski, D., Mazurek, L.: Secure multiparty computations on Bitcoin. Commun. ACM 59(4), 76\u201384 (2016)","journal-title":"Commun. ACM"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","volume-title":"Principles of Security and Trust","author":"N Atzei","year":"2017","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum Smart Contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-89722-6_9","volume-title":"Principles of Security and Trust","author":"N Atzei","year":"2018","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T., Lande, S., Zunino, R.: SoK: unraveling bitcoin smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 217\u2013242. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-89722-6_9"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-662-58387-6_29","volume-title":"Financial Cryptography and Data Security","author":"N Atzei","year":"2018","unstructured":"Atzei, N., Bartoletti, M., Lande, S., Zunino, R.: A formal model of Bitcoin transactions. In: Meiklejohn, S., Sako, K. (eds.) FC 2018. LNCS, vol. 10957, pp. 541\u2013560. Springer, Heidelberg (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-662-58387-6_29"},{"key":"10_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-319-45741-3_14","volume-title":"Computer Security \u2013 ESORICS 2016","author":"W Banasik","year":"2016","unstructured":"Banasik, W., Dziembowski, S., Malinowski, D.: Efficient zero-knowledge contingent payments in cryptocurrencies without scripts. In: Askoxylakis, I., Ioannidis, S., Katsikas, S., Meadows, C. (eds.) ESORICS 2016. LNCS, vol. 9879, pp. 261\u2013280. Springer, Cham (2016). \n                    https:\/\/doi.org\/10.1007\/978-3-319-45741-3_14"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"432","DOI":"10.1007\/978-3-030-03427-6_32","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"M Bartoletti","year":"2018","unstructured":"Bartoletti, M., Cimoli, T., Zunino, R.: Fun with Bitcoin smart contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 432\u2013449. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-03427-6_32"},{"key":"10_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-70278-0_15","volume-title":"Financial Cryptography and Data Security","author":"M Bartoletti","year":"2017","unstructured":"Bartoletti, M., Zunino, R.: Constant-deposit multiparty lotteries on Bitcoin. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 231\u2013247. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-70278-0_15"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Zunino, R.: BitML: a calculus for Bitcoin smart contracts. In: ACM SIGSAC CCS, pp. 83\u2013100. ACM (2018)","DOI":"10.1145\/3243734.3243795"},{"key":"10_CR15","unstructured":"Bartoletti, M., Zunino, R.: Verifying liquidity of Bitcoin contracts. Cryptology ePrint Archive, Report 2018\/1125 (2018). \n                    https:\/\/eprint.iacr.org\/2018\/1125"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200\u2013236. Springer, Heidelberg (2004). \n                    https:\/\/doi.org\/10.1007\/978-3-540-30080-9_7\n                    \n                  . \n                    http:\/\/www.it.uu.se\/research\/group\/darts\/papers\/texts\/new-tutorial.pdf"},{"key":"10_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-662-44381-1_24","volume-title":"Advances in Cryptology \u2013 CRYPTO 2014","author":"I Bentov","year":"2014","unstructured":"Bentov, I., Kumaresan, R.: How to use Bitcoin to design fair protocols. In: Garay, J.A., Gennaro, R. (eds.) CRYPTO 2014. LNCS, vol. 8617, pp. 421\u2013439. Springer, Heidelberg (2014). \n                    https:\/\/doi.org\/10.1007\/978-3-662-44381-1_24"},{"key":"10_CR18","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts. In: PLAS (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"10_CR19","unstructured":"Buterin, V.: Ethereum: a next generation smart contract and decentralized application platform (2013). \n                    https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"Gilad, Y., Hemo, R., Micali, S., Vlachos, G., Zeldovich, N.: Algorand: scaling byzantine agreements for cryptocurrencies. In: Symposium on Operating Systems Principles, pp. 51\u201368 (2017)","DOI":"10.1145\/3132747.3132757"},{"key":"10_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-96145-3_4","volume-title":"Computer Aided Verification","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: Foundations and tools for the static analysis of Ethereum smart contracts. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 51\u201378. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-96145-3_4"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"10_CR23","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum Virtual Machine. In: IEEE Computer Security Foundations Symposium (CSF), pp. 204\u2013217. IEEE Computer Society (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the Ethereum Virtual Machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). \n                    https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-030-00305-0_3","volume-title":"Data Privacy Management, Cryptocurrencies and Blockchain Technology","author":"R Klomp","year":"2018","unstructured":"Klomp, R., Bracciali, A.: On symbolic verification of Bitcoin\u2019s script language. In: Garcia-Alfaro, J., Herrera-Joancomart\u00ed, J., Livraga, G., Rios, R. (eds.) DPM\/CBT -2018. LNCS, vol. 11025, pp. 38\u201356. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-00305-0_3"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Kumaresan, R., Bentov, I.: How to use Bitcoin to incentivize correct computations. In: ACM CCS, pp. 30\u201341 (2014)","DOI":"10.1145\/2660267.2660380"},{"key":"10_CR27","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM CCS, pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"10_CR28","unstructured":"Maxwell, G.: The first successful zero-knowledge contingent payment (2016). \n                    https:\/\/bitcoincore.org\/en\/2016\/02\/26\/zero-knowledge-contingent-payments-announcement\/"},{"key":"10_CR29","doi-asserted-by":"crossref","unstructured":"Miller, A., Bentov, I.: Zero-collateral lotteries in Bitcoin and Ethereum. In: EuroS&P Workshops, pp. 4\u201313 (2017)","DOI":"10.1109\/EuroSPW.2017.44"},{"key":"10_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-030-03427-6_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"A Miller","year":"2018","unstructured":"Miller, A., Cai, Z., Jha, S.: Smart contracts and opportunities for formal methods. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 280\u2013299. Springer, Cham (2018). \n                    https:\/\/doi.org\/10.1007\/978-3-030-03427-6_22"},{"key":"10_CR31","unstructured":"Mythril (2018). \n                    https:\/\/github.com\/ConsenSys\/mythril"},{"key":"10_CR32","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). \n                    https:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"10_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higherorderlogic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higherorderlogic, vol. 2283. Springer Science & Business Media, Heidelberg (2002). \n                    https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"10_CR34","unstructured":"Rocket, T.: Snowflake to avalanche: a novel metastable consensus protocol family for cryptocurrencies (2018). \n                    https:\/\/avalanchelabs.org\/avalanche.pdf"},{"key":"10_CR35","doi-asserted-by":"crossref","unstructured":"Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: ACM CCS, pp. 67\u201382 (2018)","DOI":"10.1145\/3243734.3243780"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17138-4_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:17:21Z","timestamp":1558343841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17138-4_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171377","9783030171384"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17138-4_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"POST","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Principles of Security and Trust","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"post2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/post","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}