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

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. Formalizing non-sequential processes for strong adversaries is not easy. Actually, existing security analyses using the task-PIOA framework are for cryptographic protocols (e.g., the EGL oblivious transfer) only against simple adversaries (e.g., honest but curious adversary). For example, there is no case study for digital signature against strong active adversaries (i.e., EUF-CMA) in the task-PIOA framework. In this paper, we propose the first formalization of digital signature against EUF-CMA in the task-PIOA framework. To formalize the non-sequential process of EUF-CMA, we introduce a new technique for the iteration of an identical action in a single session. 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.