2026-08-14T15:21:08Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:1415 2024-03-06T11:07:45Z ddc:004 open_access

Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol Backes, Michael Maffei, Matteo Unruh, Dominique Language-based security zero-knowledge proofs applied pi-calculus direct anonymous attestation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Michael Backes and Matteo Maffei and Dominique Unruh 2008 Is Part Of Dagstuhl Seminar Proceedings, Volume 7421, Formal Protocol Verification Applied (2008) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.07421.4 urn:nbn:de:0030-drops-14153 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.07421.4 eng https://creativecommons.org/licenses/by/4.0/legalcode