Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol
Zero-Knowledge in the Applied Pi-calculus and Automated Verification of the Direct Anonymous Attestation Protocol
复制标题
DOI：
10.1109/sp.2008.23
复制
发表时间：
2008-05
期刊：
影响因子：
--
通讯作者：
M. Backes;Matteo Maffei;Dominique Unruh
中科院分区：
文献类型：
--
作者：
M. Backes;Matteo Maffei;Dominique Unruh
我们设计了一种对零知识协议的抽象，这对完全机械化的分析是可用的。抽象在应用的圆周率演算中被形式化，使用抽象地描述零知识证明的密码语义的新的方程理论。我们给出了一种从方程理论到适用于自动协议验证工具ProVerif的收敛重写系统的编码。编码是健全的和完全自动化的。我们成功地使用ProVerif获得了对直接匿名证明(DAA)协议的第一个机械化分析(简化的变体)。这要求我们设计基于互动游戏的复杂密码安全定义的新颖抽象。该分析报告了对DAA的一次新型攻击，但其现有的密码安全证明中忽略了这一点。我们提出了DAA的一个修改的变体，我们使用ProVerif成功地证明了它是安全的。
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 (a simplified variant of) the Direct Anonymous Attestation (DAA) protocol. This required us to devise 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.