arnold beckmann
blockchain
Publication Types:
Verification of Bitcoin’s Smart Contracts in Agda using Weakest Preconditions for Access Control
This paper addresses the verification of Bitcoin smart contracts using the interactive theorem prover Agda. It focuses on two standard smart contracts that govern the distribution of Bitcoins, Pay to Public Key Hash (P2PKH) and Pay to Multisig (P2MS). Both are written in Bitcoin’s low-level language script, and provide the security property of access control to the distribution of Bitcoins.
The paper introduces an operational semantics of the script commands used in P2PKH and P2MS, and formalises it in the Agda proof assistant using Hoare triples. It advocates weakest preconditions in the context of Hoare triples as the appropriate notion for verifying access control. Two methodologies for obtaining human-readable weakest preconditions are discussed in order to close the validation gap between user requirements and formal specification of smart contracts: (1) a step-by-step approach, which works backwards instruction by instruction through a script, sometimes stepping over several instructions in one go; (2) symbolic execution of the code and translation into a nested case distinction, which allows to read off weakest preconditions as the disjunction of accepting paths. A syntax for equational reasoning with Hoare Triples is defined in order to formalise those approaches in Agda.
Modeling and Computing Available Rights for Algorithmic Licensing of Movies based on Blockchain
We consider the challenge of determining which rights are available for licensing within the context of algorithmic licensing of movies using blockchain technology. We model the space of rights using set theory. We define algorithms within our modelling context that implement basic transactions for our use case, and argue for their correctness. We evaluate our algorithms through experiments within a multi-node Hyperledger Fabric network, and establish the feasibility of our algorithms for the intended use case.
Cyber-Physical Trust Systems Driven by Blockchain
Cyber Physical Trust Systems (CPTS) are Cyber Physical Systems and Internet of Things enriched with trust as an explicit, measurable, testable and verifiable system component. In this paper, we propose to use blockchain, a distributed ledger technology, as the trust enabling system component for CPTS. We propose two schemes for CPTSs driven by blockchain in relation to two typical network model cases. We show that our proposed approach achieves the security properties, such as device identification, authentication, integrity, and non-repudiation, and provides protection against popular attacks, such as replay and spoofing. We provide formal proofs of those properties using the Tamarin Prover tool. We describe results of a proof-of-concept which implements a CPTS driven by blockchain for physical asset management and present a performance analysis of our implementation. We identify use cases in which CPTSs driven by blockchain find applications.
Blockchain‐Based Cyber Physical Trust Systems
Cyber Physical Trust Systems (CPTS) are Cyber Physical Systems and Internet of Things enriched with trust as an explicit, measurable, testable system component. In this chapter, we propose to use blockchain technology as the trust enabling system component for CPTS. Our proposed approach shows that a blockchain based CPTS achieves the security properties of data authenticity, identity and integrity. We describe results of a testbed which implements a blockchain based CPTS for physical asset management.