Scopul nostru este sprijinirea şi promovarea cercetării ştiinţifice şi facilitarea comunicării între cercetătorii români din întreaga lume.
Autori: Michael Backes, Catalin Hritcu, and Matteo Maffei
Editorial: ACM Press, 15th ACM Conference on Computer and Communications Security (CCS 2008), 2008.
This paper presents the first type system for statically analyzing security
protocols that are based on zero-knowledge proofs. We show how certain
properties offered by zero-knowledge proofs can be characterized in terms of
authorization policies and statically enforced by a type system. The analysis is
modular and compositional, and provides security proofs for an unbounded number
of protocol executions. We develop a new type-checker that conducts the analysis
in a fully automated manner. We exemplify the applicability of our technique to
real-world protocols by verifying the authenticity and secrecy properties of the
Direct Anonymous Attestation (DAA) protocol. The analysis of DAA takes less than three
Cuvinte cheie: formal methods, language-based security, security protocols, type-systems, protocol verification, authentication, secrecy, zero-knowledge proofs