{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T01:46:57Z","timestamp":1770342417738,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":52,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,10,15]],"date-time":"2018-10-15T00:00:00Z","timestamp":1539561600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,10,15]]},"DOI":"10.1145\/3243734.3243795","type":"proceedings-article","created":{"date-parts":[[2018,10,16]],"date-time":"2018-10-16T12:56:36Z","timestamp":1539694596000},"page":"83-100","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":43,"title":["BitML"],"prefix":"10.1145","author":[{"given":"Massimo","family":"Bartoletti","sequence":"first","affiliation":[{"name":"University of Cagliari, Cagliari, Italy"}]},{"given":"Roberto","family":"Zunino","sequence":"additional","affiliation":[{"name":"University of Trento, Trento, Italy"}]}],"member":"320","published-online":{"date-parts":[[2018,10,15]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2794418.2794756"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3190508.3190538"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44774-1_8"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2014.35"},{"key":"e_1_3_2_2_5_1","volume-title":"Hijacking Bitcoin: Routing Attacks on Cryptocurrencies. In IEEE Symp. on Security and Privacy. 375--392","author":"Apostolaki Maria","year":"2017"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"e_1_3_2_2_7_1","volume-title":"Principles of Security and Trust (POST) (LNCS)","author":"Atzei Nicola"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Nicola Atzei Massimo Bartoletti Stefano Lande and Roberto Zunino. 2018b. A formal model of Bitcoin transactions. In Financial Cryptography and Data Security .  Nicola Atzei Massimo Bartoletti Stefano Lande and Roberto Zunino. 2018b. A formal model of Bitcoin transactions. In Financial Cryptography and Data Security .","DOI":"10.1007\/978-3-662-58387-6_29"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Christian Badertscher Ueli Maurer Daniel Tschudi and Vassilis Zikas. 2017. Bitcoin as a Transaction Ledger: A Composable Treatment. In CRYPTO. 324--356.  Christian Badertscher Ueli Maurer Daniel Tschudi and Vassilis Zikas. 2017. Bitcoin as a Transaction Ledger: A Composable Treatment. In CRYPTO. 324--356.","DOI":"10.1007\/978-3-319-63688-7_11"},{"key":"e_1_3_2_2_10_1","volume-title":"ESORICS (LNCS)","author":"Banasik Waclaw"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_31"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_15"},{"key":"e_1_3_2_2_13_1","first-page":"122","article-title":"BitML: a Calculus for Bitcoin Smart Contracts","volume":"2018","author":"Bartoletti Massimo","year":"2018","journal-title":"IACR Cryptology ePrint Archive"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/168588.168596"},{"key":"e_1_3_2_2_15_1","volume-title":"CRYPTO (LNCS)","author":"Bentov Iddo"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_2_2_17_1","volume-title":"Findel: Secure Derivative Contracts for Ethereum. In Financial Cryptography Workshops (LNCS)","volume":"10323","author":"Biryukov Alex","year":"2017"},{"key":"e_1_3_2_2_18_1","unstructured":"BitFury group. 2015. Smart Contracts on Bitcoin Blockchain. http:\/\/bitfury.com\/content\/5-white-papers-research\/contracts-1.1.1.pdf.  BitFury group. 2015. Smart Contracts on Bitcoin Blockchain. http:\/\/bitfury.com\/content\/5-white-papers-research\/contracts-1.1.1.pdf."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/646765.704125"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2015.14"},{"key":"e_1_3_2_2_21_1","unstructured":"Vitalik Buterin. 2013. Ethereum: a next generation smart contract and decentralized application platform. https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper .  Vitalik Buterin. 2013. Ethereum: a next generation smart contract and decentralized application platform. https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper ."},{"key":"e_1_3_2_2_22_1","volume-title":"Amir Kafshdar Goharshady, and Yaron Velner","author":"Chatterjee Krishnendu","year":"2018"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737997"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21741-3_1"},{"key":"e_1_3_2_2_25_1","volume-title":"A fair protocol for data trading based on Bitcoin transactions. Future Generation Computer Systems","author":"Delgado-Segura Sergi","year":"2017"},{"key":"e_1_3_2_2_26_1","volume-title":"Financial Cryptography (LNCS)","author":"Eyal Ittay"},{"key":"e_1_3_2_2_27_1","volume-title":"EUROCRYPT (LNCS)","author":"Garay Juan A."},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-009-0094-1"},{"key":"e_1_3_2_2_29_1","volume-title":"CAV (LNCS)","author":"Grishchenko Ilya"},{"key":"e_1_3_2_2_30_1","volume-title":"Principles of Security and Trust (POST) (LNCS)","author":"Grishchenko Ilya"},{"key":"e_1_3_2_2_31_1","volume-title":"Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In Financial Cryptography Workshops (LNCS)","volume":"10323","author":"Hirai Yoichi","year":"2017"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351267"},{"key":"e_1_3_2_2_33_1","volume-title":"Hawk: The Blockchain Model of Cryptography and Privacy-Preserving Smart Contracts. In IEEE Symp. on Security and Privacy. 839--858","author":"Kosba Ahmed E.","year":"2016"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660380"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2810103.2813712"},{"key":"e_1_3_2_2_36_1","unstructured":"Eric Lombrozo Johnson Lau and Pieter Wuille. 2015. Segregated Witness (Consensus layer). BIP 141 https:\/\/github.com\/bitcoin\/bips\/blob\/master\/bip-0141.mediawiki.  Eric Lombrozo Johnson Lau and Pieter Wuille. 2015. Segregated Witness (Consensus layer). BIP 141 https:\/\/github.com\/bitcoin\/bips\/blob\/master\/bip-0141.mediawiki."},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Anastasia Mavridou and Aron Laszka. 2018. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Financial Cryptography and Data Security .  Anastasia Mavridou and Aron Laszka. 2018. Designing Secure Ethereum Smart Contracts: A Finite State Machine Based Approach. In Financial Cryptography and Data Security .","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"e_1_3_2_2_39_1","unstructured":"Gregory Maxwell. 2016. The first successful Zero-Knowledge Contingent Payment. https:\/\/bitcoincore.org\/en\/2016\/02\/26\/zero-knowledge-contingent-payments-announcement\/.  Gregory Maxwell. 2016. The first successful Zero-Knowledge Contingent Payment. https:\/\/bitcoincore.org\/en\/2016\/02\/26\/zero-knowledge-contingent-payments-announcement\/."},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Andrew Miller and Iddo Bentov. 2017. Zero-Collateral Lotteries in Bitcoin and Ethereum. In EuroS&P Workshops. 4--13.  Andrew Miller and Iddo Bentov. 2017. Zero-Collateral Lotteries in Bitcoin and Ethereum. In EuroS&P Workshops. 4--13.","DOI":"10.1109\/EuroSPW.2017.44"},{"key":"e_1_3_2_2_41_1","volume-title":"Sprites: Payment Channels that Go Faster than Lightning. CoRR","author":"Miller Andrew","year":"2017"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-53357-4_9"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"crossref","unstructured":"Xavier Nicollin and Joseph Sifakis. 1991. An Overview and Synthesis on Timed Process Algebras. In CAV. 376--398.   Xavier Nicollin and Joseph Sifakis. 1991. An Overview and Synthesis on Timed Process Algebras. In CAV. 376--398.","DOI":"10.1007\/3-540-55179-4_36"},{"key":"e_1_3_2_2_44_1","volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3139337.3139340"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-70278-0_12"},{"key":"e_1_3_2_2_47_1","unstructured":"Joseph Poon and Thaddeus Dryja. 2015. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. https:\/\/lightning.network\/lightning-network-paper.pdf  Joseph Poon and Thaddeus Dryja. 2015. The Bitcoin Lightning Network: Scalable Off-Chain Instant Payments. https:\/\/lightning.network\/lightning-network-paper.pdf"},{"key":"e_1_3_2_2_48_1","volume-title":"Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR","author":"Sergey Ilya","year":"2018"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_2_50_1","volume-title":"Weakly Secret Bit Commitment: Applications to Lotteries and Fair Exchange","author":"Syverson Paul F."},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.5210\/fm.v2i9.548"},{"key":"e_1_3_2_2_52_1","volume-title":"Dana Drachsler Cohen, Arthur Gervais, Florian Buenzli, and Martin T. Vechev.","author":"Tsankov Petar","year":"2018"}],"event":{"name":"CCS '18: 2018 ACM SIGSAC Conference on Computer and Communications Security","location":"Toronto Canada","acronym":"CCS '18","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243734.3243795","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3243734.3243795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:08:18Z","timestamp":1750212498000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3243734.3243795"}},"subtitle":["A Calculus for Bitcoin Smart Contracts"],"short-title":[],"issued":{"date-parts":[[2018,10,15]]},"references-count":52,"alternative-id":["10.1145\/3243734.3243795","10.1145\/3243734"],"URL":"https:\/\/doi.org\/10.1145\/3243734.3243795","relation":{},"subject":[],"published":{"date-parts":[[2018,10,15]]},"assertion":[{"value":"2018-10-15","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}