Cryptology ePrint Archive: Report 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.

Category / Keywords: implementation / public ledgers, formal verification, proverif, fstar

Original Publication (in the same form): Workshop on Security Protocol Implementations: Development and Analysis

Date: received 4 May 2018

Contact author: nadim at symbolic software

Available format(s): PDF | BibTeX Citation

Version: 20180510:203904 (All versions of this report)

Short URL: ia.cr/2018/416


[ Cryptology ePrint archive ]