Abstract
Many real-world protocols, such as SSL/TLS, SSH, IPsec, DNSSEC, IEEE 802.11i, and Kerberos, derive new keys from other keys. To be able to analyze such protocols in a composable way, in this paper we extend an ideal functionality for symmetric and public-key encryption proposed in previous work by a mechanism for key derivation. We also equip this functionality with message authentication codes (MACs), digital signatures, and ideal nonce generation. We show that the resulting 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 this new functionality, we identify sufficient criteria for protocols to provide universally composable key exchange and secure channels. Since these criteria are based on the new 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.
This work was partially supported by the DFG under Grant KU 1434/5-1 and KU 1434/6-1.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Backes, M., Dürmuth, M., Küsters, R.: On Simulatability Soundness and Mapping Soundness of Symbolic Cryptography. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol. 4855, pp. 108–120. Springer, Heidelberg (2007)
Backes, M., Pfitzmann, B.: Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library. In: CSFW-17 2004, pp. 204–218. IEEE Computer Society, Los Alamitos (2004)
Bellare, M., Pointcheval, D., Rogaway, P.: Authenticated Key Exchange Secure against Dictionary Attacks. In: Preneel, B. (ed.) EUROCRYPT 2000. LNCS, vol. 1807, pp. 139–155. Springer, Heidelberg (2000)
Bellare, M., Rogaway, P.: Provably Secure Session Key Distribution: The Three Party Case. In: STOC 1995, pp. 57–66. ACM, New York (1995)
Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically Verified Implementations for TLS. In: CCS 2008, pp. 459–468. ACM, New York (2008)
Black, J., Rogaway, P., Shrimpton, T.: Encryption-Scheme Security in the Presence of Key-Dependent Messages. In: Nyberg, K., Heys, H.M. (eds.) SAC 2002. LNCS, vol. 2595, pp. 62–75. Springer, Heidelberg (2003)
Blanchet, B., Jaggard, A.D., Scedrov, A., Tsay, J.-K.: Computationally Sound Mechanized Proofs for Basic and Public-key Kerberos. In: ASIACCS 2008, pp. 87–99. ACM, New York (2008)
Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: FOCS 2001, pp. 136–145. IEEE Computer Society, Los Alamitos (2001)
Canetti, R.: Universally Composable Signature, Certification, and Authentication. In: CSFW-17 2004, pp. 219–233. IEEE Computer Society, Los Alamitos (2004)
Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols, Technical Report 2000/067, Cryptology ePrint Archive (December 2005), http://eprint.iacr.org/2000/067/
Canetti, R., Krawczyk, H.: Security Analysis of IKE’s Signature-Based Key-Exchange Protocol. In: Yung, M. (ed.) CRYPTO 2002. LNCS, vol. 2442, pp. 143–161. Springer, Heidelberg (2002)
Canetti, R., Krawczyk, H.: Universally Composable Notions of Key Exchange and Secure Channels. In: Knudsen, L.R. (ed.) EUROCRYPT 2002. LNCS, vol. 2332, pp. 337–351. Springer, Heidelberg (2002)
Canetti, R., Rabin, T.: Universal Composition with Joint State. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 265–281. Springer, Heidelberg (2003)
Comon-Lundh, H., Cortier, V.: Computational soundness of observational equivalence. Technical Report INRIA Research Report RR-6508, INRIA (2008), http://www.loria.fr/~cortier/Papiers/CCS08-report.pdf
Cortier, V., Kremer, S., Küsters, R., Warinschi, B.: Computationally Sound Symbolic Secrecy in the Presence of Hash Functions. In: Arun-Kumar, S., Garg, N. (eds.) FSTTCS 2006. LNCS, vol. 4337, pp. 176–187. Springer, Heidelberg (2006)
Gajek, S., Manulis, M., Pereira, O., Sadeghi, A., Schwenk, J.: Universally Composable Security Analysis of TLS. In: Baek, J., Bao, F., Chen, K., Lai, X. (eds.) ProvSec 2008. LNCS, vol. 5324, pp. 313–327. Springer, Heidelberg (2008)
He, C., Mitchell, J.C.: Security Analysis and Improvements for IEEE 802.11i. In: NDSS 2005, The Internet Society (2005)
He, C., Sundararajan, M., Datta, A., Derek, A., Mitchell, J.C.: A Modular Correctness Proof of IEEE 802.11i and TLS. In: CCS 2005, pp. 2–15. ACM, New York (2005)
Hofheinz, D., Unruh, D., Müller-Quade, J.: Polynomial Runtime and Composability. Technical Report 2009/023, Cryptology ePrint Archive (2009), http://eprint.iacr.org/2009/023/
IEEE Standard 802.11-2007. Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications, Part 11 of IEEE Standard for Information technology – Telecommunications and information exchange between systems – Local and metropolitan area networks – Specific requirements (June 2007)
Kobara, K., Shin, S., Strefler, M.: Partnership in key exchange protocols. In: ASIACCS 2009, pp. 161–170. ACM, New York (2009)
Küsters, R.: Simulation-Based Security with Inexhaustible Interactive Turing Machines. In: CSFW-19 2006, pp. 309–320. IEEE Computer Society, Los Alamitos (2006)
Küsters, R., Tuengerthal, M.: Joint State Theorems for Public-Key Encryption and Digitial Signature Functionalities with Local Computation. In: CSF 2008, pp. 270–284. IEEE Computer Society, Los Alamitos (2008)
Küsters, R., Tuengerthal, M.: Computational Soundness for Key Exchange Protocols with Symmetric Encryption. In: CCS 2009, pp. 91–100. ACM Press, New York (2009)
Küsters, R., Tuengerthal, M.: Universally Composable Symmetric Encryption. In: CSF 2009, pp. 293–307. IEEE Computer Society, Los Alamitos (2009)
Küsters, R., Tuengerthal, M.: Ideal Key Derivation and Encryption in Simulation-based Security. Technical Report 2010/295, Cryptology ePrint Archive (2010), http://eprint.iacr.org/2010/295/
Micciancio, D., Warinschi, B.: Soundness of Formal Encryption in the Presence of Active Adversaries. In: Naor, M. (ed.) TCC 2004. LNCS, vol. 2951, pp. 133–151. Springer, Heidelberg (2004)
Morrissey, P., Smart, N.P., Warinschi, B.: A Modular Security Analysis of the TLS Handshake Protocol. In: Pieprzyk, J. (ed.) ASIACRYPT 2008. LNCS, vol. 5350, pp. 55–73. Springer, Heidelberg (2008)
Ohigashi, T., Morii, M.: A Practical Message Falsification Attack on WPA. In: JWIS 2009 (2009)
Pfitzmann, B., Waidner, M.: A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission. In: S&P 2001, pp. 184–201. IEEE Computer Society, Los Alamitos (2001)
Roy, A., Datta, A., Derek, A., Mitchell, J.C.: Inductive Proofs of Computational Secrecy. In: Biskup, J., López, J. (eds.) ESORICS 2007. LNCS, vol. 4734, pp. 219–234. Springer, Heidelberg (2007)
Tews, E., Beck, M.: Practical Attacks against WEP and WPA. In: WISEC 2009, pp. 79–86. ACM, New York (2009)
Zhang, F., Ma, J., Moon, S.: The Security Proof of a 4-Way Handshake Protocol in IEEE 802.11i. In: Hao, Y., Liu, J., Wang, Y.-P., Cheung, Y.-m., Yin, H., Jiao, L., Ma, J., Jiao, Y.-C. (eds.) CIS 2005. LNCS (LNAI), vol. 3802, pp. 488–493. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Küsters, R., Tuengerthal, M. (2011). Ideal Key Derivation and Encryption in Simulation-Based Security. In: Kiayias, A. (eds) Topics in Cryptology – CT-RSA 2011. CT-RSA 2011. Lecture Notes in Computer Science, vol 6558. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19074-2_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-19074-2_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-19073-5
Online ISBN: 978-3-642-19074-2
eBook Packages: Computer ScienceComputer Science (R0)