Search Results

Documents authored by Maffei, Matteo

Document
DOI: 10.4230/LIPIcs.AFT.2026.1
BitVM: Quasi-Turing Complete Computation on Bitcoin

Authors: Lukas Aumayr, Zeta Avarikioti, Robin Linus Woll, Matteo Maffei, Andrea Pelosi, Christos Stefo, and Alexei Zamyatin

Published in: LIPIcs, Volume 395, 8th Conference on Advances in Financial Technologies (AFT 2026)

Abstract
A long-standing question in the blockchain community is which class of computations is efficiently expressible in cryptocurrencies with limited scripting languages, such as Bitcoin Script. Such languages expose a reduced trusted computing base, thereby being less prone to hacks and vulnerabilities, but have long been believed to support only limited classes of payments. In this work, we confute this long-standing belief by showing for the first time that arbitrary computations can be encoded in today’s Bitcoin Script without introducing any language modification or additional security assumptions, such as trusted hardware, trusted parties, or committees with an honest majority. We present BitVM, a two-party protocol that realizes a generic virtual machine by combining cryptographic primitives and economic incentives. We conduct a formal analysis of BitVM, characterizing its functionality, system assumptions, and security properties. We further demonstrate the practicality of our approach by implementing a prototype and performing an experimental evaluation: in the optimistic case (i.e., when parties agree), our protocol requires just three on-chain transactions, whereas in the pessimistic case, the number of transactions grows logarithmically with the size of the virtual machine. We exemplify the deployment potential of BitVM by building a Bitcoin-sidechain bridge application. This work not only solves a long-standing theoretical problem, but it also promises a strong practical impact, enabling the development of complex applications in Bitcoin.
Cite as

Lukas Aumayr, Zeta Avarikioti, Robin Linus Woll, Matteo Maffei, Andrea Pelosi, Christos Stefo, and Alexei Zamyatin. BitVM: Quasi-Turing Complete Computation on Bitcoin. In 8th Conference on Advances in Financial Technologies (AFT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 395, pp. 1:1-1:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{aumayr_et_al:LIPIcs.AFT.2026.1,
  author =	{Aumayr, Lukas and Avarikioti, Zeta and Woll, Robin Linus and Maffei, Matteo and Pelosi, Andrea and Stefo, Christos and Zamyatin, Alexei},
  title =	{{BitVM: Quasi-Turing Complete Computation on Bitcoin}},
  booktitle =	{8th Conference on Advances in Financial Technologies (AFT 2026)},
  pages =	{1:1--1:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-451-2},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{395},
  editor =	{Kiayias, Aggelos and Kyropoulou, Maria},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.AFT.2026.1},
  URN =		{urn:nbn:de:0030-drops-278556},
  doi =		{10.4230/LIPIcs.AFT.2026.1},
  annote =	{Keywords: Bitcoin, quasi-Turing completeness, off-chain protocols, bridge}
}
Document
DOI: 10.4230/DagRep.11.9.80
Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)

Authors: Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu

Published in: Dagstuhl Reports, Volume 11, Issue 9 (2022)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21431 "Rigorous Methods for Smart Contracts". Blockchain technologies have emerged as an exciting field for both researchers and practitioners focusing on formal guarantees for software. It is arguably a "once in a lifetime" opportunity for rigorous methods to be integrated in audit processes for parties deploying smart contracts, whether for fund raising, securities trading, or supply-chain management. Smart contracts are programs managing cryptocurrency accounts on a blockchain. Research in the area of smart contracts includes a fascinating combination of formal methods, programming-language semantics, and cryptography. First, there is vibrant development of verification and program-analysis techniques that check the correctness of smart-contract code. Second, there are emerging designs of programming languages and methodologies for writing smart contracts such that they are more robust by construction or more amenable to analysis and verification. Programming-language abstraction layers expose low-level cryptographic primitives enabling developers to design high-level cryptographic protocols. Automated-reasoning mechanisms present a common underlying enabler; and the specific needs of the smart-contract world offer new challenges. This workshop brought together stakeholders in the aforementioned areas related to advancing reliable smart-contract technologies.
Cite as

Nikolaj S. Bjørner, Maria Christakis, Matteo Maffei, and Grigore Rosu. Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431). In Dagstuhl Reports, Volume 11, Issue 9, pp. 80-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Article{bjrner_et_al:DagRep.11.9.80,
  author =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  title =	{{Rigorous Methods for Smart Contracts (Dagstuhl Seminar 21431)}},
  pages =	{80--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{9},
  editor =	{Bj{\o}rner, Nikolaj S. and Christakis, Maria and Maffei, Matteo and Rosu, Grigore},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.9.80},
  URN =		{urn:nbn:de:0030-drops-159198},
  doi =		{10.4230/DagRep.11.9.80},
  annote =	{Keywords: automated reasoning, cryptographic protocols, program verification, programming languages, smart contracts}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.352
Computationally Sound Abstraction and Verification of Secure Multi-Party Computations

Authors: Michael Backes, Matteo Maffei, and Esfandiar Mohammadi

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
We devise an abstraction of secure multi-party computations in the applied $\pi$-calculus. Based on this abstraction, we propose a methodology to mechanically analyze the security of cryptographic protocols employing secure multi-party computations. We exemplify the applicability of our framework by analyzing the SIMAP sugar-beet double auction protocol. We finally study the computational soundness of our abstraction, proving that the analysis of protocols expressed in the applied $\pi$-calculus and based on our abstraction provides computational security guarantees.
Cite as

Michael Backes, Matteo Maffei, and Esfandiar Mohammadi. Computationally Sound Abstraction and Verification of Secure Multi-Party Computations. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 352-363, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{backes_et_al:LIPIcs.FSTTCS.2010.352,
  author =	{Backes, Michael and Maffei, Matteo and Mohammadi, Esfandiar},
  title =	{{Computationally Sound Abstraction and Verification of Secure Multi-Party  Computations}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{352--363},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.352},
  URN =		{urn:nbn:de:0030-drops-28771},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.352},
  annote =	{Keywords: Computational soundness, Secure multi-party computation, Process calculi, Protocol verification}
}
Document
DOI: 10.4230/DagSemProc.07421.4
Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol

Authors: Michael Backes, Matteo Maffei, and Dominique Unruh

Published in: Dagstuhl Seminar Proceedings, Volume 7421, Formal Protocol Verification Applied (2008)

Abstract
We devise an abstraction of zero-knowledge protocols that is accessible to a fully mechanized analysis. The abstraction is formalized within the applied pi-calculus using a novel equational theory that abstractly characterizes the cryptographic semantics of zero-knowledge proofs. We present an encoding from the equational theory into a convergent rewriting system that is suitable for the automated protocol verifier ProVerif. The encoding is sound and fully automated. We successfully used ProVerif to obtain the first mechanized analysis of the Direct Anonymous Attestation (DAA) protocol. The analysis in particular required us to devise novel abstractions of sophisticated cryptographic security definitions based on interactive games.
Cite as

Michael Backes, Matteo Maffei, and Dominique Unruh. Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol. In Formal Protocol Verification Applied. Dagstuhl Seminar Proceedings, Volume 7421, pp. 1-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{backes_et_al:DagSemProc.07421.4,
  author =	{Backes, Michael and Maffei, Matteo and Unruh, Dominique},
  title =	{{Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol}},
  booktitle =	{Formal Protocol Verification Applied},
  pages =	{1--43},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{7421},
  editor =	{Liqun Chen and Steve Kremer and Mark D. Ryan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07421.4},
  URN =		{urn:nbn:de:0030-drops-14153},
  doi =		{10.4230/DagSemProc.07421.4},
  annote =	{Keywords: Language-based security, zero-knowledge proofs, applied pi-calculus, direct anonymous attestation}
}

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact