Abstracts - 2007
Task-PIOAs and Security Verification
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Sayan Mitra, Olivier Pereira & Roberto Segala
The framework of Probabilistic Input/Output Automata (PIOA) is a simple combination of I/O automata and Markov decision processes. PIOAs are well-suited for the analysis of distributed algorithms that use randomness as a computational primitive. Typically, each participating process is modeled as an automaton with randomized transitions, while the entire protocol is modeled as the (asynchronous) parallel composition of all participants.
This modeling paradigm combines nondeterministic and probabilistic choices in a very natural way. This is attractive because, in our experience, nondeterminism plays several important roles in modeling and verification. It provides a convincing option for modeling timing uncertainties in a distributed and highly unpredictable environment. Using proof techniques such invariant assertions and simulation relations, we obtain correctness guarantees that are independent of the relative timing of certain events. Moreover, nondeterminism allows us to model systems at high levels of abstraction, where many details are left unspecified. These features in turn support descriptions of system decomposition, both ``horizontally'' (based on parallel composition) and ``vertically'' (based on levels of abstraction).
In this project, we develop the Task-PIOA framework, with security verification as a target application [1,2,3]. Task-PIOA uses a task-based scheduling mechanism that is less powerful than the traditional perfect-information scheduler. As a result, cryptographic protocols may be specified with nondeterminism, yet without the danger of introducing semantic inconsistencies such as hidden information flow.
In order to model computational assumptions, we augment Task-PIOA with time bounds on both the description of an automaton and the length of task schedules [1,4,5]. We also define an approximate implementation relation that captures the notion of computational indistinguishability. A variant of probabilistic simulation relations is proposed, and shown to be sound for proving approximate implementation. This is a useful technique for proving that a real system correctly implements an abstract specification.
In , we model a well-known two-party Oblivious Transfer (OT) protocol  and prove its correctness. We show that a real system, consisting of two protocol parties and an adversarial communication service, implements an ideal system, consisting of an OT ideal functionality and a simulator. This says, roughly, that every possible behavior of the real protocol can be simulated using interactions with the ideal functionality.
The OT case studies follows the general outline of simulation-based security, which has been studied quite extensively (see, e.g., ). In [8,9], we give a generic formulation of simulation-based security, which we call secure emulation. We show that secure emulation is preserved under concurrent composition, with any polynomial number of substitutions.
Another interesting discovery is that the move from sequential scheduling, as used in many other frameworks, to task-based nondeterministic scheduling has some nontrivial consequences. In fact, the same syntactic definition of simulation-based security gives rise to different semantic notions, depending on which scheduling mechanism is adopted. Several examples are presented in , along with a proof that unbounded forwarders are definable in Task-PIOA and hence several important notions of security collapse.
Finally, we are able to formulate statistical indistinguishability as an implementation relation in the Task-PIOA framework, which can then be proven using approximate simulation relations . This technique separates proof obligations into two categories: those requiring probabilistic reasoning, as well as those that do not. The latter is a good candidate for mechanization. We illustrate this general method by verifying the statistical zero knowledge property of a well-known identification protocol proposed by Girault, Poupard and Stern .
 R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol. Cryptology ePrint Archive Report 2005/452, December 2005.
 R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Task-Structured Probabilistic I/O Automata. In Proceedings of the 8th International Workshop on Discrete Event Systems (WODES'06), July 2006.
 R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Task-Structured Probabilistic I/O Automata. Submitted for journal publication.
 R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Time-bounded Task-PIOAs: A Framework for Analyzing Security Protocols''. In Proceedings of the 20th International Symposium on Distributed Computing (DISC 2006), September 2006.
 R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Analyzing Security Protocols Using Time-Bounded Task-PIOAs. Submitted for journal publication.
 O. Goldreich, S. Micali, and A. Wigderson. How to play any mental game. Proc. 19th STOC, pp. 218--229, 1987.
 A. Datta, R. Kuesters, J. C. Mitchell, A. Ramanathan. On the Relationship between Notions of Simulation-Based Security. In Proceedings of Theory of Cryptography Conference (TCC), 2005.
 L. Cheung, D. Kaynar, N. Lynch and O. Pereira. Compositional Security for Task-PIOAs. Under review.
 R. Canetti, L. Cheung, N. Lynch and O. Pereira. On the Role of Scheduling in Simulation-Based Security. Accepted at the Workshop on Issues in the Theory of Security (WITS), March 2007.
 L. Cheung, S. Mitra and O. Pereira. Verifying Statistical Zero Knowledge with Approximate Implementations. Under review.
 M. Girault, G. Poupard and J. Stern. On the Fly Authentication and Signature Schemes Based on Groups of Unknown Order. Journal of Cryptology 19(4):463---487, 2006.