Backes, Michael ;
Maffei, Matteo ;
Unruh, Dominique
Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol
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: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/opus/volltexte/2008/1415},
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}
}
|
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 |
14.04.2008
