Ideal Key Derivation and Encryption in Simulation-based Security
Ralf Küsters and Max Tuengerthal
Many real-world protocols, such as SSL/TLS, SSH, IPsec, IEEE 802.11i, DNSSEC, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend our ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip our functionality with message authentication codes (MACs) and ideal nonce generation. We show that our ideal functionality can be realized based on standard cryptographic assumptions and constructions, hence, providing a solid foundation for faithful, composable cryptographic analysis of real-world security protocols. Based on our functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on our ideal functionality, checking the criteria requires merely information-theoretic or even only syntactical arguments, rather than involved reduction arguments. As a case study, we use our method to analyze two central protocols of the IEEE 802.11i standard, namely the 4-Way Handshake Protocol and the CCM Protocol, proving composable security properties. As to the best of our knowledge, this constitutes the first rigorous cryptographic analysis of these protocols.