License
when quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-14153
URL: http://drops.dagstuhl.de/opus/volltexte/2008/1415/

Backes, Michael ; Maffei, Matteo ; Unruh, Dominique

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

pdf-format:
Dokument 1.pdf (343 KB)


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.

BibTeX - Entry

@InProceedings{backes_et_al:DSP:2008:1415,
  author =	{Michael Backes and Matteo Maffei and Dominique Unruh},
  title =	{Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol},
  booktitle =	{Formal Protocol Verification Applied},
  year =	{2008},
  editor =	{Liqun Chen and Steve Kremer and Mark D. Ryan},
  number =	{07421},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Internationales Begegnungs- und Forschungszentrum f{\"u}r Informatik (IBFI), Schloss Dagstuhl, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1415},
  annote =	{Keywords: Language-based security, zero-knowledge proofs, applied pi-calculus, direct anonymous attestation}
}

Keywords: Language-based security, zero-knowledge proofs, applied pi-calculus, direct anonymous attestation
Seminar: 07421 - Formal Protocol Verification Applied
Issue date: 2008
Date of publication: 14.04.2008


DROPS-Home | Fulltext Search | Imprint Published by LZI