Composable Protocols for the Cloud

In the first part of the talk, we motivate and present a framework for the modular design and analysis of protocols for Cloud applications.Clouds are highly complex systems. Numerous cryptographic modules run in concurrent processes and interact with other, non-cryptographic parts (e.g., caches, browsers, policy enforcers, users) of the system.

A major problem here is scalability because the analytical complexity linearly grows with the number of modules. A natural approach to coping with the blow up is automation and mechanization. Composability allows applying the automated tool only to small components while still obtaining a global security guarantee.

In the second part of talk, we choose from the framework a cryptographic module, the Diffie-Hellman key exchange, and automatically assert security properties of the single-session key exchange protocol while deducing the security of the composite,multi-session system. Specifically, we show how to automatically assert forward secrecy under fully adaptive party corruptions, while maintaining both composability and cryptographic soundness.