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

https://hal.inria.fr/hal-01948971
Contributor : Nadim Kobeissi <>
Submitted on : Sunday, December 9, 2018 - 12:33:04 PM
Last modification on : Saturday, December 15, 2018 - 1:10:40 AM
Long-term archiving on: : Sunday, March 10, 2019 - 12:24:13 PM

File

ldl_short.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01948971, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

62

Files downloads

172