Compositional Security for Task-PIOAs

Task-PIOA is a modeling framework for distributed systems with both probabilistic and nondeterministic behaviors. It is suitable for cryptographic applications because its task-based scheduling mechanism is less powerful than the traditional perfect-information scheduler. Moreover, one can speak of two types of complexity restrictions: time bounds on description of task-PIOAs and time bounds on length of schedules. This distinction, along with the flexibility of nondeterministic specifications, are interesting departures from existing formal frameworks for computational security. The current paper presents a new approximate implementation relation for task-PIOAs. This relation is transitive and is preserved under hiding of external actions. Also, it is shown to be preserved under concurrent composition, with any polynomial number of substitutions. Building upon this foundation, we present the notion of structures, which classifies communications into two categories: those with a distinguisher environment and those with an adversary. We then formulate secure emulation in the spirit of traditional simulation-based security, and a composition theorem follows as a corollary of the composition theorem for the new approximate implementation relation.