Formal modeling of random oracle programmability and verification of signature unforgeability using task-PIOAs

Abstract

Thetask-structured Probabilistic I/OAutomata (task-PIOA) framework provides a method to formulate and to prove the computationally- bounded security of non-sequential processing systems in a formalway. 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.