OASIcs.FMBC.2020.5.pdf
- Filesize: 446 kB
- 13 pages
Document
A Blockchain Model in Tamarin and Formal Analysis of Hash Time Lock Contract
Authors
-
Part of:
Volume:
2nd Workshop on Formal Methods for Blockchains (FMBC 2020)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-12-11
Cite AsGet BibTex
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)
https://doi.org/10.4230/OASIcs.FMBC.2020.5
https://doi.org/10.4230/OASIcs.FMBC.2020.5
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.
Subject Classification
ACM Subject Classification
- Security and privacy → Formal security models
Keywords
- Blockchain model
- Tamarin
- Hash time lock contract
- Formal verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, and Łukasz Mazurek. Fair two-party computations via bitcoin deposits. In Rainer Böhme, Michael Brenner, Tyler Moore, and Matthew Smith, editors, Financial Cryptography and Data Security, pages 105-121, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.
-
Marcin Andrychowicz, Stefan Dziembowski, Daniel Malinowski, and Łukasz Mazurek. Modeling bitcoin contracts by timed automata. In Axel Legay and Marius Bozga, editors, Formal Modeling and Analysis of Timed Systems, pages 7-22, Cham, 2014. Springer International Publishing.
- Iddo Bentov, Yan Ji, Fan Zhang, Lorenz Breidenbach, Philip Daian, and Ari Juels. Tesseract: Real-time cryptocurrency exchange using trusted hardware. In Lorenzo Cavallaro et al., editors, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, pages 1521-1538. ACM, 2019. URL: https://doi.org/10.1145/3319535.3363221.
- Sergiu Bursuc and Steve Kremer. Contingent payments on a public ledger: models and reductions for automated verification. In ESORICS 2019 - The 24th European Symposium on Research in Computer Security, Luxembourg, Luxembourg, September 2019. URL: https://hal.archives-ouvertes.fr/hal-02269063.
-
Christian Decker and Roger Wattenhofer. A fast and scalable payment network with bitcoin duplex micropayment channels. In Andrzej Pelc and Alexander A. Schwarzmann, editors, Stabilization, Safety, and Security of Distributed Systems, pages 3-18, Cham, 2015. Springer International Publishing.
- Thaddeus Dryja Joseph Poon. The Bitcoin Lightning Network: Scalable off-chain instant payments, 2016. URL: https://lightning.network/lightning-network-paper.pdf.
- Gregory Maxwell. Zero knowledge contingent payments, 2011. URL: https://en.bitcoin.it/wiki/Zero%20Knowledge%20Contingent%20Payment.
-
Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The tamarin prover for the symbolic analysis of security protocols. In Proceedings of the 25th International Conference on Computer Aided Verification - Volume 8044, CAV 2013, page 696–701, Berlin, Heidelberg, 2013. Springer-Verlag.
- Tianyu Sun and Wensheng Yu. A formal verification framework for security issues of blockchain smart contracts. Electronics, 9:255, February 2020. URL: https://doi.org/10.3390/electronics9020255.
-
Mathieu Turuani, Thomas Voegtlin, and Michael Rusinowitch. Automated verification of electrum wallet. In Jeremy Clark, Sarah Meiklejohn, Peter Y.A. Ryan, Dan Wallach, Michael Brenner, and Kurt Rohloff, editors, Financial Cryptography and Data Security, pages 27-42, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg.