Skip to main content
SpringerLink
Log in
Book cover

International Conference on Information Security and Cryptology

ICISC 2014: Information Security and Cryptology - ICISC 2014 pp 37–52Cite as

Formal Modeling of Random Oracle Programmability and Verification of Signature Unforgeability Using Task-PIOAs

  • Conference paper
  • First Online:

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

Abstract

The task-structured Probabilistic I/O Automata (task-PIOA) framework provides a method to formulate and to prove the computationally-bounded security of non-sequential processing systems in a formal way. Though existing works show security analyses of some classic cryptographic protocols (e.g., the EGL oblivious transfer) against simple adversaries (e.g., honest but curious adversary), there is no case study for fundamental cryptographic primitives (e.g., encryption and signature) against sufficiently strong adversaries (e.g., IND-CCA for encryption and EUF-CMA for signature). In this paper, we propose a formulation of signature against EUF-CMA in the task-PIOA framework. Using the task-PIOA framework allows us to verify security of signature schemes in the non-sequential scheduling manner. We show the validity and usefulness of our formulation by giving a formal security analysis of the FDH signature scheme. In order to prove the security, we also introduce a method to utilize the power of random oracles. As far as we know, this work is the first case study to clarify usefulness of random oracles in this framework.

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

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 EPUB and 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

Learn about institutional subscriptions

References

  1. Dolev, D., Yao, A.C.C.: On the security of public key protocols. In: FOCS 1981, pp. 350–357 (1981)

    Google Scholar 

  2. Abadi, M., Rogaway, P.: Reconciling two views of cryptography (the computational soundness of formal encryption). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

  4. Cortier, V., Warinschi, B.: Computationally sound, automated proofs for security protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Canetti, R.: Universally composable security: a new paradigm for cryptographic protocols. In: FOCS 2001, pp. 136–145 (2001). Full version is at http://eprint.iacr.org/2000/067

  6. Canetti, R., Herzog, J.: Universally composable symbolic analysis of mutual authentication and key-exchange protocols (extended abstrast). In: Halevi, S., Rabin, T. (eds.) TCC 2006. LNCS, vol. 3876, pp. 380–403. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

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

  8. Mitchell, J.C., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theor. Comput. Sci. 353, 118–164 (2006)

    Article  MATH  MathSciNet  Google Scholar 

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

  10. Canetti, R., Cheung, L., Kaynar, D.K., Liskov, M., Lynch, N.A., Pereira, O., Segala, R.: Using task-structured probabilistic I/O automata to analyze an oblivious transfer protocol. Technical report, MIT CSAIL-TR-2007-011 (2007)

    Google Scholar 

  11. Canetti, R., Cheung, L., Kaynar, D.K., Liskov, M., Lynch, N.A., Pereira, O., Segala, R.: Analyzing security protocols using time-bounded task-PIOAs. Discrete Event Dyn. Syst. 18(1), 111–159 (2008)

    Article  MATH  Google Scholar 

  12. Yoneyama, K., Kokubun, Y., Ohta, K.: A security analysis on Diffie-Hellman key exchange against adaptive adversaries using task-structured PIOA. In: FCS-ARSPA 2007, pp. 131–148 (2007)

    Google Scholar 

  13. Cheung, L., Mitra, S., Pereira, O.: Verifying statistical zero knowledge with approximate implementations. In: Cryptology ePrint Archive 2007/195 (2007)

    Google Scholar 

  14. Jaggard, A.D., Meadows, C., Mislove, M., Segala, R.: Reasoning about probabilistic security using task-PIOAs. In: Armando, A., Lowe, G. (eds.) ARSPA-WITS 2010. LNCS, vol. 6186, pp. 2–22. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  15. Canetti, R., Goldreich, O., Halevi, S.: The random oracle methodology, revisited (preliminary version). In: STOC 1998, pp. 209–218 (1998)

    Google Scholar 

  16. Bellare, M., Rogaway, P.: Random oracles are practical: a paradigm for designing efficient protocols. In: ACM Conference on Computer and Communications Security 1993, pp. 62–73 (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. NTT Secure Platform Laboratories, 3-9-11 Midori-cho Musashino-shi, Tokyo, 180-8585, Japan

    Kazuki Yoneyama

Authors
  1. Kazuki Yoneyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kazuki Yoneyama .

Editor information

Editors and Affiliations

  1. Sejong University, Seoul, Korea, Republic of (South Korea)

    Jooyoung Lee

  2. Kookmin University, Seoul, Korea, Republic of (South Korea)

    Jongsung Kim

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Yoneyama, K. (2015). Formal Modeling of Random Oracle Programmability and Verification of Signature Unforgeability Using Task-PIOAs. In: Lee, J., Kim, J. (eds) Information Security and Cryptology - ICISC 2014. ICISC 2014. Lecture Notes in Computer Science(), vol 8949. Springer, Cham. https://doi.org/10.1007/978-3-319-15943-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15943-0_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-15942-3

  • Online ISBN: 978-3-319-15943-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation