Search Results

Documents authored by Maffei, Matteo

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}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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