Paper 2019/443

Contingent payments on a public ledger: models and reductions for automated verification

Sergiu Bursuc and Steve Kremer

Abstract

We study protocols that rely on a public ledger infrastructure, concentrating on protocols for zero-knowledge contingent payment, whose security properties combine diverse notions of fairness and privacy. We argue that rigorous models are required for capturing the ledger semantics, the protocol-ledger interaction, the cryptographic primitives and, ultimately, the security properties one would like to achieve. Our focus is on a particular level of abstraction, where network messages are represented by a term algebra, protocol execution by state transition systems (e.g. multiset rewrite rules) and where the properties of interest can be analyzed with automated verification tools. We propose models for: (1) the rules guiding the ledger execution, taking the coin functionality of public ledgers such as Bitcoin as an example; (2) the security properties expected from ledger-based zero-knowledge contingent payment protocols; (3) two different security protocols that aim at achieving these properties relying on different ledger infrastructures; (4) reductions that allow simpler term algebras for homomorphic cryptographic schemes. Altogether, these models allow us to derive a first automated verification for ledger-based zero-knowledge contingent payment using the Tamarin prover. Furthermore, our models help in clarifying certain underlying assumptions, security and efficiency tradeoffs that should be taken into account when deploying protocols on the blockchain.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Preprint. Minor revision.
Keywords
fair exchangesecurity modelsblockchainautomated security proofselectronic commerce and payment
Contact author(s)
sergiu bursuc @ inria fr
steve kremer @ inria fr
History
2019-05-08: received
Short URL
https://ia.cr/2019/443
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2019/443,
      author = {Sergiu Bursuc and Steve Kremer},
      title = {Contingent payments on a public ledger: models and reductions for automated verification},
      howpublished = {Cryptology ePrint Archive, Paper 2019/443},
      year = {2019},
      note = {\url{https://eprint.iacr.org/2019/443}},
      url = {https://eprint.iacr.org/2019/443}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.