Analysis of modern cryptographic applications

One of the central challenges in the analysis of complex and industrial-size systems is the capability to deal with complex cryptographic operations. While academic protocols traditionally relied only on basic and well understood cryptographic operations such as encryption and digital signatures, modern applications make usage of sophisticated cryptographic primitives offering complex security features that go far beyond traditional properties such as the secrecy and authenticity of a communication. Zero-knowledge proofs constitute the most prominent and arguably most amazing example of such primitives. A zero-knowledge proof consists of a message or a sequence of messages that combines two seemingly contradictory properties: First, it constitutes a proof of a statement that cannot be forged, i.e., it is impossible, or at least computationally infeasible, to produce a zero-knowledge proof of a wrong statement; Second, a zero-knowledge proof does not reveal any information besides the bare fact that the statement is valid. Modern applications rely on zero-knowledge proofs to achieve complex, and sometimes seemingly conflicting, security properties, for instance authenticity and anonymity.
This talk presents some recent results in the analysis of distributed applications, with a particular focus on protocols based on zero-knowledge proofs. In particular, we present an abstraction technique for protocols based on zero-knowledge proofs that is amenable to automated verification. The abstraction is formalized within a process calculus using a novel equational theory that characterizes the cryptographic semantics of zero-knowledge proofs. We show how certain properties offered by zero-knowledge proofs can be characterized in terms of authorization policies and automatically enforced by a type system. The analysis is efficient and compositional.