Paper 2007/289

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

Michael Backes, Matteo Maffei, and Dominique Unruh

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.

Metadata
Available format(s)
PDF
Category
Foundations
Publication info
Published elsewhere. Unknown where it was published
Keywords
zero-knowledgeabstractionmechanized analysisdirect anonymous attestationDAA
Contact author(s)
backes @ cs uni-sb de
History
2007-08-07: received
Short URL
https://ia.cr/2007/289
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2007/289,
      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},
      howpublished = {Cryptology ePrint Archive, Paper 2007/289},
      year = {2007},
      note = {\url{https://eprint.iacr.org/2007/289}},
      url = {https://eprint.iacr.org/2007/289}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.