Skip to Main content Skip to Navigation
Conference papers

Ledger Design Language: Designing and Deploying Formally Verified Public Ledgers

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 .
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Nadim Kobeissi Connect in order to contact the contributor
Submitted on : Sunday, December 9, 2018 - 12:33:04 PM
Last modification on : Wednesday, June 8, 2022 - 12:50:04 PM
Long-term archiving on: : Sunday, March 10, 2019 - 12:24:13 PM


Files produced by the author(s)


  • HAL Id : hal-01948971, version 1



Nadim Kobeissi, Natalia Kulatova. Ledger Design Language: Designing and Deploying Formally Verified Public Ledgers. Workshop on Security Protocol Implementations: Development and Analysis, Apr 2018, London, United Kingdom. ⟨hal-01948971⟩



Record views


Files downloads