DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2020.5

A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract

Authors: Colin Boyd, Kristian Gjøsteen, and Shuang Wu

Published in: OASIcs, Volume 84, 2nd Workshop on Formal Methods for Blockchains (FMBC 2020)

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.

Cite as

Colin Boyd, Kristian Gjøsteen, and Shuang Wu. A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract. In 2nd Workshop on Formal Methods for Blockchains (FMBC 2020). Open Access Series in Informatics (OASIcs), Volume 84, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{boyd_et_al:OASIcs.FMBC.2020.5,
  author =	{Boyd, Colin and Gj{\o}steen, Kristian and Wu, Shuang},
  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 =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-169-6},
  ISSN =	{2190-6807},
  year =	{2020},
  volume =	{84},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2020.5},
  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}
}

Search Results

Documents authored by Gjøsteen, Kristian

A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract

Abstract

Cite as

Thanks for your feedback!

Could not send message