in IEEE Symposium on Security and Privacy, Proceedings of SSP'08, pp. 202-215, May 2008. Preprint on IACR ePrint 2007/289.
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.
This publication is accompanied by links to downloadable versions of this publication. These documents do not necessarily correspond exactly to the cited version. Instead, in most cases full, updated or preliminary versions are provided. For access to the official version, follow the "Official version" link to the publishers site.
Slides used in my talks are available upon personal request, as long as you agree not to disseminate them to a wider audience or make them available online. If in doubt, please ask.