License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.FMBC.2020.5
URN: urn:nbn:de:0030-drops-134187
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13418/
Boyd, Colin ;
Gjøsteen, Kristian ;
Wu, Shuang
A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract
Abstract
Formal analysis and verification methods can aid the design and validation of security properties in blockchain based protocols. However, to generate a reasonable and correct verification, a proper model for the blockchain is needed. In this paper, we give a blockchain model in Tamarin. Based on our model we analyze and give a formal verification for the hash time lock contract, an atomic cross chain trading protocol. The result shows that our model is able to identify an underlying assumption for the hash time lock contract and that the model is useful for analyzing blockchain based protocols.
BibTeX - Entry
@InProceedings{boyd_et_al:OASIcs:2020:13418,
author = {Colin Boyd and Kristian Gj{\o}steen and Shuang Wu},
title = {{A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract}},
booktitle = {2nd Workshop on Formal Methods for Blockchains (FMBC 2020)},
pages = {5:1--5:13},
series = {OpenAccess Series in Informatics (OASIcs)},
ISBN = {978-3-95977-169-6},
ISSN = {2190-6807},
year = {2020},
volume = {84},
editor = {Bruno Bernardo and Diego Marmsoler},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/13418},
URN = {urn:nbn:de:0030-drops-134187},
doi = {10.4230/OASIcs.FMBC.2020.5},
annote = {Keywords: Blockchain model, Tamarin, Hash time lock contract, Formal verification}
}
