On Formal Verification of Arithmetic-Based Cryptographic Primitives | SpringerLink
Skip to main content
Springer Nature Link
Log in

On Formal Verification of Arithmetic-Based Cryptographic Primitives

  • Conference paper
Information Security and Cryptology – ICISC 2008 (ICISC 2008)

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

Included in the following conference series:

Abstract

Cryptographic primitives are fundamental for information security: they are used as basic components for cryptographic protocols or public-key cryptosystems. In many cases, their security proofs consist in showing that they are reducible to computationally hard problems. Those reductions can be subtle and tedious, and thus not easily checkable. On top of the proof assistant Coq, we had implemented in previous work a toolbox for writing and checking game-based security proofs of cryptographic primitives. In this paper we describe its extension with number-theoretic capabilities so that it is now possible to write and check arithmetic-based cryptographic primitives in our toolbox. We illustrate our work by machine checking the game-based proofs of unpredictability of the pseudo-random bit generator of Blum, Blum and Shub, and semantic security of the public-key cryptographic scheme of Goldwasser and Micali.

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

Access this chapter

Log in via an institution

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., Tanaka, M., Marti, N.: Formal proof of provable security by game-playing in a proof assistant. In: Susilo, W., Liu, J.K., Mu, Y. (eds.) ProvSec 2007. LNCS, vol. 4784, pp. 151–168. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  2. Backes, M., Berg, M., Unruh, D.: A formal language for cryptographic pseudocode. In: 4th Workshop on Formal and Computational Cryptography (FCC 2008) (2008)

    Google Scholar 

  3. Barthe, G., Grégoire, B., Janvier, R., Olmedo, F., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: 4th Workshop on Formal and Computational Cryptography (FCC 2008) (2008)

    Google Scholar 

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

    Google Scholar 

  5. Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: Proceedings of the 14th IEEE Computer Security Foundations Workshop (CSFW-14), pp. 82–96. IEEE Computer Society, Los Alamitos (2001)

    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 15(2), 364–383 (1986); an earlier version appeared in Proceedings of Crypto 1982

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  9. Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Théry, L.: A modular formalisation of finite group theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 86–101. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Halevi, S.: A plausible approach to computer-aided cryptographic proofs. Cryptology ePrint Archive, Report 2005/181 (2005)

    Google Scholar 

  11. Knuth, D.E.: The Art of Computer Programming – Seminumerical Algorithms, vol. 2. Addison-Wesley, Reading (1969)

    MATH  Google Scholar 

  12. Lafourcade, P., Lakhnech, Y., Ene, C., Courant, J., Daubignard, M.: Towards automated proofs of asymmetric encryption schemes in the random oracle model. In: Proceedings of the 2008 ACM Conference on Computer and Communications Security, ACM, New York (2008) (to appear)

    Google Scholar 

  13. 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); also available as Cryptology ePrint Archive, Report 2007/199

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  16. Vazirani, U.V., Vazirani, V.V.: Efficient and secure pseudo-random number generation. In: Proceedings of the IEEE 25th Annual Symposium on Foundations of Computer Science (FOCS 1984), pp. 458–463. IEEE Computer Society, Los Alamitos (1984)

    Google Scholar 

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

Download references

Author information

Authors and Affiliations

  1. Research Center for Information Security, AIST, Japan

    David Nowak

Authors
  1. David Nowak
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Electronic and Electrical Engineering, Pohang University of Science and Technology (POSTECH), San 31 Hyoja-dong, Nam-gu,, 790-784, Pohang, Kyungbuk, Korea

    Pil Joong Lee

  2. Department of Mathematical Sciences, Seoul National University, 599 Gwanakno, Gwanak-gu, 151-742, Seoul, Korea

    Jung Hee Cheon

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Nowak, D. (2009). On Formal Verification of Arithmetic-Based Cryptographic Primitives. In: Lee, P.J., Cheon, J.H. (eds) Information Security and Cryptology – ICISC 2008. ICISC 2008. Lecture Notes in Computer Science, vol 5461. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00730-9_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-00730-9_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-00729-3

  • Online ISBN: 978-3-642-00730-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics