2026-07-26T20:55:47Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:13418 2024-03-12T11:59:41Z ddc:004 open_access

A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract Boyd, Colin Gjøsteen, Kristian Wu, Shuang Blockchain model Tamarin Hash time lock contract Formal verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Colin Boyd and Kristian Gjøsteen and Shuang Wu 2020 Is Part Of OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.FMBC.2020.5 urn:nbn:de:0030-drops-134187 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.5 eng https://creativecommons.org/licenses/by/3.0/legalcode