DROPS

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}
}

Search Results

Documents authored by Backes, Michael

Computationally Sound Abstraction and Verification of Secure Multi-Party Computations

Abstract

Cite as

Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol

Abstract

Cite as

Thanks for your feedback!

Could not send message