Skip to main content

Ideal Key Derivation and Encryption in Simulation-Based Security

  • Conference paper
Topics in Cryptology – CT-RSA 2011 (CT-RSA 2011)

Part of the book series: Lecture Notes in Computer Science ((LNSC,volume 6558))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Chapter  Google Scholar 

  2. 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)

    Google Scholar 

  3. 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)

    Chapter  Google Scholar 

  4. Bellare, M., Rogaway, P.: Provably Secure Session Key Distribution: The Three Party Case. In: STOC 1995, pp. 57–66. ACM, New York (1995)

    Google Scholar 

  5. Bhargavan, K., Fournet, C., Corin, R., Zalinescu, E.: Cryptographically Verified Implementations for TLS. In: CCS 2008, pp. 459–468. ACM, New York (2008)

    Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. 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)

    Google Scholar 

  8. Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: FOCS 2001, pp. 136–145. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  9. Canetti, R.: Universally Composable Signature, Certification, and Authentication. In: CSFW-17 2004, pp. 219–233. IEEE Computer Society, Los Alamitos (2004)

    Google Scholar 

  10. 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/

  11. 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)

    Chapter  Google Scholar 

  12. 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)

    Chapter  Google Scholar 

  13. Canetti, R., Rabin, T.: Universal Composition with Joint State. In: Boneh, D. (ed.) CRYPTO 2003. LNCS, vol. 2729, pp. 265–281. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  14. 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

  15. 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)

    Chapter  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. He, C., Mitchell, J.C.: Security Analysis and Improvements for IEEE 802.11i. In: NDSS 2005, The Internet Society (2005)

    Google Scholar 

  18. 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)

    Google Scholar 

  19. 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/

  20. 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)

    Google Scholar 

  21. Kobara, K., Shin, S., Strefler, M.: Partnership in key exchange protocols. In: ASIACCS 2009, pp. 161–170. ACM, New York (2009)

    Google Scholar 

  22. Küsters, R.: Simulation-Based Security with Inexhaustible Interactive Turing Machines. In: CSFW-19 2006, pp. 309–320. IEEE Computer Society, Los Alamitos (2006)

    Google Scholar 

  23. 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)

    Google Scholar 

  24. 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)

    Google Scholar 

  25. Küsters, R., Tuengerthal, M.: Universally Composable Symmetric Encryption. In: CSF 2009, pp. 293–307. IEEE Computer Society, Los Alamitos (2009)

    Google Scholar 

  26. 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/

  27. 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)

    Chapter  Google Scholar 

  28. 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)

    Chapter  Google Scholar 

  29. Ohigashi, T., Morii, M.: A Practical Message Falsification Attack on WPA. In: JWIS 2009 (2009)

    Google Scholar 

  30. 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)

    Google Scholar 

  31. 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)

    Chapter  Google Scholar 

  32. Tews, E., Beck, M.: Practical Attacks against WEP and WPA. In: WISEC 2009, pp. 79–86. ACM, New York (2009)

    Google Scholar 

  33. 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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics