Paper 2018/416

Ledger Design Language: Towards Formal Reasoning and Implementation for Public Ledgers

Nadim Kobeissi and Natalia Kulatova

Abstract

Cryptocurrencies have popularized public ledgers, known colloquially as "blockchains". While the Bitcoin blockchain is relatively simple to reason about as, effectively, a hash chain, more complex public ledgers are largely designed without any formalization of desired cryptographic properties such as authentication or integrity. These designs are then implemented without assurances against real-world bugs leading to little assurance with regards to practical, real-world security. Ledger Design Language (LDL) is a modeling language for describing public ledgers. The LDL compiler produces two outputs. The first output is a an applied-pi calculus symbolic model representing the public ledger as a protocol. Using ProVerif, the protocol can be played against an active attacker, whereupon we can query for block integrity, authenticity and other properties. The second output is a formally verified read/write API for interacting with the public ledger in the real world, written in the F* programming language. F* features such as dependent types allow us to validate a block on the public ledger, for example, by type-checking it so that its signing public key be a point on a curve. Using LDL's outputs, public ledger designers obtain automated assurances on the theoretical coherence and the real-world security of their designs with a single framework based on a single modeling language.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. Workshop on Security Protocol Implementations: Development and Analysis
Keywords
public ledgersformal verificationproveriffstar
Contact author(s)
nadim @ symbolic software
History
2018-05-10: received
Short URL
https://ia.cr/2018/416
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2018/416,
      author = {Nadim Kobeissi and Natalia Kulatova},
      title = {Ledger Design Language: Towards Formal Reasoning and Implementation for Public Ledgers},
      howpublished = {Cryptology ePrint Archive, Paper 2018/416},
      year = {2018},
      note = {\url{https://eprint.iacr.org/2018/416}},
      url = {https://eprint.iacr.org/2018/416}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.