A Calculus for Game-Based Security Proofs | SpringerLink
Skip to main content
Springer Nature Link
Log in

A Calculus for Game-Based Security Proofs

  • Conference paper
Provable Security (ProvSec 2010)

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

Included in the following conference series:

Abstract

The game-based approach to security proofs in cryptography is a widely-used methodology for writing proofs rigorously. However a unifying language for writing games is still missing. In this paper we show how CSLR, a probabilistic lambda-calculus with a type system that guarantees that computations are probabilistic polynomial time, can be equipped with a notion of game indistinguishability. This allows us to define cryptographic constructions, effective adversaries, security notions, computational assumptions, game transformations, and game-based security proofs in the unified framework provided by CSLR. Our code for cryptographic constructions is close to implementation in the sense that we do not assume arbitrary uniform distributions but use a realistic algorithm to approximate them. We illustrate our calculus on cryptographic constructions for public-key encryption and pseudorandom bit generation.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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.

Similar content being viewed by others

References

  1. Affeldt, R., Nowak, D., Yamada, K.: Certifying assembly with formal cryptographic proofs: the case of BBS. In: Proceedings of the 9th International Workshop on Automated Verification of Critical Systems, AVoCS 2009 (2009)

    Google Scholar 

  2. Backes, M., Berg, M., Unruh, D.: A formal language for cryptographic pseudocode. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 353–376. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Barthe, G., Grégoire, B., Zanella Béguelin, S.: Formal certification of code-based cryptographic proofs. In: Proceedings of the 36th ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL 2009), pp. 90–101. ACM Press, New York (2009)

    Google Scholar 

  4. Bellantoni, S., Cook, S.A.: A new recursion-theoretic characterization of the polytime functions. In: Computational Complexity, vol. 2, pp. 97–110 (1992)

    Google Scholar 

  5. Bellare, M., Namprempre, C.: Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm. Journal of Cryptology 21, 469–491 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  6. Blanchet, B., Pointcheval, D.: Automated security proofs with sequences of games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Blum, L., Blum, M., Shub, M.: A simple unpredictable pseudo random number generator. SIAM Journal on Computing. Society for Industrial and Applied Mathematics 15(2), 364–383 (1986)

    MATH  Google Scholar 

  8. Boneh, D.: The Decision Diffie-Hellman problem. In: Buhler, J.P. (ed.) ANTS 1998. LNCS, vol. 1423, pp. 48–83. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  9. Bellare, M., Rogaway, P.: Code-based game-playing proofs and the security of triple encryption. Cryptology ePrint Archive, Report 2004/331 (2004)

    Google Scholar 

  10. Corin, R., den Hartog, J.: A probabilistic Hoare-style logic for game-based cryptographic proofs. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 252–263. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Courant, J., Daubignard, M., Ene, C., Lafourcade, P., Lakhnech, Y.: Towards automated proofs for asymmetric encryption schemes in the random oracle model. In: Proceedings of the 15th ACM Conference Computer and Communications Security, CCS 2008, pp. 371–380. ACM Press, New York (2008)

    Chapter  Google Scholar 

  12. Diffie, W., Hellman, M.E.: New directions in cryptography. IEEE Transactions on Information Theory 22(6), 644–654 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  13. Elgamal, T.: A public key cryptosystem and a signature scheme based on discrete logarithms. IEEE Transactions on Information Theory 31(4), 469–472 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  14. Goldreich, O.: The Foundations of Cryptography: Basic Tools. Cambridge University Press, Cambridge (2001)

    Book  MATH  Google Scholar 

  15. Goldwasser, S., Micali, S.: Probabilistic encryption. Journal of Computer and System Sciences (JCSS) 28(2), 270–299 (1984) (An earlier version appeared in proceedings of STOC 1982)

    Google Scholar 

  16. Hofmann, M.: A Mixed Modal/Linear Lambda Calculus with Applications to Bellantoni-Cook Safe Recursion. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 275–294. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  17. Hofmann, M.: Safe recursion with higher types and BCK-algebra. In: Annals of Pure and Applied Logic, vol. 1414, 104(1-3), pp. 113–166 (2000)

    Google Scholar 

  18. Hurd, J.: A formal approach to probabilistic termination. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 230–245. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Impagliazzo, R., Kapron, B.M.: Logics for reasoning about cryptographic constructions. Journal of Computer and System Sciences 72(2), 286–320 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  20. Menezes, A.J., van Oorschot, P.C., Vanstone, S.A.: Handbook of Applied Cryptography. CRC Press, Boca Raton (1996)

    Book  MATH  Google Scholar 

  21. Mitchell, J.C., Mitchell, M., Scedrov, A.: A linguistic characterization of bounded oracle computation and probabilistic polynomial time. In: Proceedings of the 39th Annual Symposium on Foundations of Computer Science (FOCS 1998), pp. 725–733 (1998)

    Google Scholar 

  22. Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science 353(1-3), 118–164 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  23. Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  24. Nowak, D.: A framework for game-based security proofs. In: Qing, S., Imai, H., Wang, G. (eds.) ICICS 2007. LNCS, vol. 4861, pp. 319–333. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  25. Nowak, D.: On formal verification of arithmetic-based cryptographic primitives. In: Lee, P.J., Cheon, J.H. (eds.) ICISC 2008. LNCS, vol. 5461, pp. 368–382. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  26. Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Proceedings of the 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2002), pp. 154–165 (2002)

    Google Scholar 

  27. Shoup, V.: Sequences of games: a tool for taming complexity in security proofs. Cryptology ePrint Archive, Report 2004/332 (2004)

    Google Scholar 

  28. Yao, A.C.: Theory and applications of trapdoor functions. In: Proceedings of the IEEE 23rd Annual Symposium on Foundations of Computer Science (FOCS 1982), pp. 80–91. IEEE, Los Alamitos (1982)

    Chapter  Google Scholar 

  29. Zhang, Y.: The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 401–415. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Center for Information Security, AIST, Japan

    David Nowak

  2. Institute of Software, Chinese Academy of Sciences, China

    Yu Zhang

Authors
  1. David Nowak
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yu Zhang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Information Science and Technology, Jalan Ayer Keroh Lama, Multimedia University, 75450, Malacca, Malaysia

    Swee-Huay Heng

  2. Department of Computer and Information Sciences, Ibaraki University, 4-12-1 Nakanarusawa, 316-8511, Hitachi, Ibaraki, Japan

    Kaoru Kurosawa

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nowak, D., Zhang, Y. (2010). A Calculus for Game-Based Security Proofs. In: Heng, SH., Kurosawa, K. (eds) Provable Security. ProvSec 2010. Lecture Notes in Computer Science, vol 6402. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16280-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16280-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16279-4

  • Online ISBN: 978-3-642-16280-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation