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

Sergiu Bursuc and Steve Kremer. Contingent payments on a public ledger: models and reductions for automated verification. In Proceedings of the 24th European Symposium on Research in Computer Security, Part I (ESORICS'19), pp. 361–382, Lecture Notes in Computer Science 11735, Springer, Luxembourg, September 2019.
doi:10.1007/978-3-030-29959-0_18

Download

[PDF] [HTML] 

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.

BibTeX

@inproceedings{BK-esorics19,
  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.  \par 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.
                  \par 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.
                  },
  address =	 {Luxembourg},
  author =	 {Bursuc, Sergiu and Kremer, Steve},
  booktitle =	 {{P}roceedings of the 24th {E}uropean {S}ymposium on
                  {R}esearch in {C}omputer {S}ecurity, Part I
                  ({ESORICS}'19)},
  month =	 sep,
  pages =	 {361--382},
  publisher =	 {Springer},
  series =	 {Lecture Notes in Computer Science},
  title =	 {Contingent payments on a public ledger: models and
                  reductions for automated verification},
  volume =	 11735,
  year =	 2019,
  acronym =	 {{ESORICS}'19},
  nmonth =	 9,
  doi =		 {10.1007/978-3-030-29959-0_18},
  url =		 {https://hal.archives-ouvertes.fr/hal-02269063/},
                  ={https://hal.archives-ouvertes.fr/hal-02269063/document},
}