Formalization of bitcoin off-chain protocols in F*

Abstract

Die Anzahl der Blockchain-Anwendungen ist in den letzten 16 Jahren enorm gewachsen und hat viele neue Forschungsbereiche geschaffen, die sich der Weiterentwicklung und Analyse dieser Technologie widmen. Eine der bekanntesten Implementierungen ist das Bitcoin-Netzwerk, das eine dezentralisierte Zahlungseinrichtung auf der Grundlage eines öffentlich zugänglichen Blockchain-Ledgers etabliert hat. Trotz seiner vielversprechenden Eigenschaften hat seine wachsende Popularität auch dazu geführt, viele Probleme und Einschränkungen des ursprünglichen Designs aufzudecken. Ein spezifisches Problem, mit dem Bitcoin konfrontiert ist, während es versucht, sich im Bereich der Decentralized Finance zu etablieren, ist seine Skalierbarkeit, um einen höheren Transaktionsdurchsatz zu bewältigen. Off-Chain-Lösungen wie das Lightning Network haben den Ansatz verfolgt, die Blockchain zu entlasten und direkte Zahlungskanäle zwischen zwei Teilnehmern aufzubauen (daher Off-Chain). Mittels eines Konsensprotokolls tauschen die Parteien gültige On-Chain-Transaktionen aus, um ihren gemeinsamen finanziellen Stand zu aktualisieren. Dies kann unbestimmt oft durchgeführt werden, wobei das endgültige Ergebnis in der Blockchain eingetragen wird. Solche Implementierungen stützen sich oft auf Timeout-Perioden, deren Einhaltung durch das Bitcoin-Netzwerk und seine Skriptsprache gewährleistet ist, sowie auf die Offenlegung geheimer Daten, um veraltete Zustände aufzuheben oder als Nachweis für erfolgreiche Zahlungen zu dienen. Mit steigender Komplexität solcher Protokolle können manuelle Beweise über deren Richtigkeit zu fehlerhaften Ergebnissen führen. In dieser Arbeit legen wir den Grundstein für eine teilautomatisierte Off-Chain-Protokollverifikation in Bitcoin unter Verwendung der Programmiersprache F*. Wir erweitern das symbolische Verifikationsframework DY* um ein Blockchain-Modell, das es ermöglicht zeitliche Garantien zu überprüfen und einen neuen Label-Typ, um geheime Werte zu kennzeichnen, die gewollt offengelegt werden sollen, ohne dabei bestehende Sicherheitsgarantien (z.B., Geheimhaltung) zu verletzen. Um die Richtigkeit des Blockchain-Systems zu überprüfen, werden eine Reihe von Lemmata, die Eigenschaften einer gültigen Blockchain beschreiben, als korrekt bewiesen. Zusätzlich stellen wir zwei einfache Protokollimplementierungen bereit, um die neu hinzugefügten Funktionalitäten vorzustellen.

The number of blockchain applications has grown immensely over the last decade, creating many new research areas dedicated to advancing and analyzing this technology. One of the most well-known implementations is the Bitcoin network, which established a decentralized payment facility, based on a publicly accessible blockchain ledger. Despite its promising features, the growth in its popularity has also led to uncovering many issues and limitations of the original design. One specific problem Bitcoin encounters as it seeks to establish itself in the Decentralized Finance sector is its ability to scale as the transaction throughput grows. Off-chain solutions, such as the Lightning Network, aim to shift the load away from the blockchain (hence off-chain) and create direct Payment Channels between principals. In this way, the parties can publish on-chain only the transaction that establishes a new channel and the one that closes the communication, while all the intermediate exchanges are handled off-chain. Through a consensus protocol, participants exchange valid on-chain transactions to update their common financial state at their discretion. Once completed, the final result is recorded on the blockchain. Such implementations often rely on timeout periods, which are enforced through the Bitcoin network and its scripting language, and the disclosure of secret data to either revoke outdated states or as proof for successful payments. As the complexity of such protocols increases, relying solely on manual reasoning for their correctness is insufficient, as it can be extremely time-consuming and error-prone. Hence, within this work, we provide the basis for a semi-automated off-chain protocol verification in Bitcoin using the proof-oriented programming language F*. We extend the symbolic verification framework DY* with a blockchain model supporting reasoning over time and introduce important modifications in the type system, allowing us to annotate secret values that will be intentionally disclosed without violating existing secrecy guarantees. To verify the correctness of the blockchain system, a set of lemmas expressing properties of a valid blockchain are proven correct. Additionally, two simple protocol implementations are provided to introduce the usage of newly added functionalities.