Top

Published in:

2020 | OriginalPaper | Chapter

UTXO\(_{\textsf {ma}}\): UTXO with Multi-asset Support

Authors : Manuel M. T. Chakravarty, James Chapman, Kenneth MacKenzie, Orestis Melkonian, Jann Müller, Michael Peyton Jones, Polina Vinogradova, Philip Wadler, Joachim Zahnentferner

Published in: Leveraging Applications of Formal Methods, Verification and Validation: Applications

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

A prominent use case of Ethereum smart contracts is the creation of a wide range of user-defined tokens or assets by way of smart contracts. User-defined assets are non-native on Ethereum; i.e., they are not directly supported by the ledger, but require repetitive custom code. This makes them unnecessarily inefficient, expensive, and complex. It also makes them insecure as numerous incidents on Ethereum have demonstrated. Even without stateful smart contracts, the lack of perfect fungibility of Bitcoin assets allows for implementing user-defined tokens as layer-two solutions, which also adds an additional layer of complexity.

In this paper, we explore an alternative design based on Bitcoin-style UTXO ledgers. Instead of introducing general scripting capabilities together with the associated security risks, we propose an extension of the UTXO model, where we replace the accounting structure of a single cryptocurrency with a new structure that manages an unbounded number of user-defined, native tokens, which we call token bundles. Token creation is controlled by forging policy scripts that, just like Bitcoin validator scripts, use a small domain-specific language with bounded computational expressiveness, thus favouring Bitcoin’s security and computational austerity. The resulting approach is lightweight, i.e., custom asset creation and transfer is cheap, and it avoids use of any global state in the form of an asset registry or similar.

The proposed UTXO\(_{\textsf {ma}}\) model and the semantics of the scripting language have been formalised in the Agda proof assistant.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Native Custom Tokens in the Extended UTXO Model

next chapter Towards Configurable and Efficient Runtime Verification of Blockchain Based Smart Contracts at the Virtual Machine Level

https://github.com/omelkonian/formal-utxo/tree/ed72.

We have chosen to represent \(\textsf {Quantities}\) as a finitely-supported function whose values are themselves finitely-supported functions (in an implementation, this would be a nested map). We did this to make the definition of the rules simpler (in particular Rule 8). However, it could equally well be defined as a finitely-supported function from tuples of \(\textsf {PolicyID}\)s and \(\textsf {Asset}\)s to \(\textsf {Quantity}\)s.

The restriction on outputs is enforced by Rule 2. We simply do not impose such a restriction on the \( forge \) field: this lets us define rules in a simpler way, with cleaner notation.

KYC stands for “know your customer”, which is the process of verifying a customer’s identity before allowing the customer to use a company’s service.

Lightning Network multi-asset channels (2016). https://github.com/lightningnetwork/lightning-rfc/pull/72

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–560. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-662-58387-6_29CrossRef

Buterin, V., Hakim, L., Rosenfeld, M., Lev, R.: Liquid: a bitcoin sidechain (2012)

Chakravarty, M.M.T., et al.: Native custom tokens in the extended UTXO model. In: Margaria,T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 89–111. Springer, Heidelberg (2020). https://omelkonian.github.io/data/publications/eutxoma.pdf

Chakravarty, M.M.T., Chapman, J., MacKenzie, K., Melkonian, O., Peyton Jones, M., Wadler, P.: The extended UTXO model. In: Bernhard, M., et al. (eds.) FC 2020. LNCS, vol. 12063, pp. 525–539. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54455-3_37CrossRef

Chakravarty, M.M.T., et al.: Hydra: fast isomorphic state channels. Technical report, Cryptology ePrint Archive, Report 2020/299 (2020). https://eprint.iacr.org/2020/299

DAML Team: DAML SDK documentation (2020). https://docs.daml.com/

Entriken, W., Shirley, D., Evans, J., Sachs, N.: ERC-721 non-fungible token standard. Ethereum Foundation (2018). https://eips.ethereum.org/EIPS/eip-721

Goodman, L.: Tezos–a self-amending crypto-ledger white paper (2014)

10.

Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/en/bitcoin-paper

11.

Nick, J., Poelstra, A., Sanders, G.: Liquid: a bitcoin sidechain (2020)

12.

Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contract intermediate-level language. arXiv preprint arXiv:1801.00687 (2018)

13.

Stellar Development Foundation: Stellar Development Guides (2020). https://solidity.readthedocs.io/

14.

Tezos Team: Digital Assets on Tezos (2020). https://assets.tqtezos.com/docs/intro/

15.

Vogelsteller, F., Buterin, V.: ERC-20 token standard. Ethereum Foundation (Stiftung Ethereum), Zug, Switzerland (2015). https://eips.ethereum.org/EIPS/eip-20

16.

Waves Team: Waves blockchain documentation (2020). https://docs.wavesprotocol.org/

17.

Xie, J.: Nervos CKB: a common knowledge base for crypto-economy (2018). https://docs.daml.com/

18.

Zahnentferner, J.: An abstract model of UTxO-based cryptocurrencies with scripts. IACR Cryptology ePrint Archive 2018, 469 (2018). https://eprint.iacr.org/2018/469

19.

Zahnentferner, J.: Multi-currency ledgers (2018). https://eprint.iacr.org/2020/895

Title: UTXO: UTXO with Multi-asset Support
Authors: Manuel M. T. Chakravarty
James Chapman
Kenneth MacKenzie
Orestis Melkonian
Jann Müller
Michael Peyton Jones
Polina Vinogradova
Philip Wadler
Joachim Zahnentferner
Publisher: Springer International Publishing
Book: Leveraging Applications of Formal Methods, Verification and Validation: Applications
Print ISBN: 978-3-030-61466-9

Electronic ISBN: 978-3-030-61467-6

Copyright Year: 2020
DOI: https://doi.org/10.1007/978-3-030-61467-6_8

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner