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
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},
}