Kavli Affiliate: James Chiang
| First 5 Authors: James Chiang, , , ,
| Summary:
Smart contracting protocols promise to regulate the transfer of
cryptocurrency amongst participants in a trustless manner. A safe smart
contract implementation should ensure that each participant can always append a
contract transaction to the blockchain in order move the contract towards
secure completion. To this goal, we propose Bitcoin Trace-Net, a contract
verification framework which generates an executable symbolic model from the
underlying contract implementation. A Trace-Net model consists of a Petri Net
formalism enriched with a Dolev-Yao-like actor knowledge model. The explicit
symbolic actor knowledge model supports the verification of contracts featuring
cryptographic sub-protocols, which may not be observable on the blockchain.
Trace-Net is sufficiently expressive to accurately model blockchain semantics
such as the delay between a transaction broadcast and its subsequent
confirmation, as well as adversarial blockchain reorganizations of finite
depths, both of which can break smart contract safety. As an implementation
level framework, Trace-Net can be instantiated at run-time to monitor and
verify smart contract protocol executions.
| Search Query: ArXiv Query: search_query=au:”James Chiang”&id_list=&start=0&max_results=10