Sciweavers

Share
SP
2008
IEEE

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

8 years 1 months ago
Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol
e an abstraction of zero-knowledge protocols that is le 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 (a simplified variant of) the Direct Anonymous Attestation (DAA) protocol. This required us e novel abstractions of sophisticated cryptographic security definitions based on interactive games. The analysis reported a novel attack on DAA that was overlooked in its existing cryptographic security proof. We propose a revised variant of DAA that we successfully prove secure using ProVerif.
Michael Backes, Matteo Maffei, Dominique Unruh
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2008
Where SP
Authors Michael Backes, Matteo Maffei, Dominique Unruh
Comments (0)
books