
Research
Abstracts  2007 
TaskPIOAs and Security VerificationRan Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Sayan Mitra, Olivier Pereira & Roberto SegalaOverviewThe framework of Probabilistic Input/Output Automata (PIOA) is a simple combination of I/O automata and Markov decision processes. PIOAs are wellsuited 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 TaskPIOA framework, with security verification as a target application [1,2,3]. TaskPIOA uses a taskbased scheduling mechanism that is less powerful than the traditional perfectinformation 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 TaskPIOA 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. ProgressIn [1], we model a wellknown twoparty Oblivious Transfer (OT) protocol [6] 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 simulationbased security, which has been studied quite extensively (see, e.g., [7]). In [8,9], we give a generic formulation of simulationbased 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 taskbased nondeterministic scheduling has some nontrivial consequences. In fact, the same syntactic definition of simulationbased security gives rise to different semantic notions, depending on which scheduling mechanism is adopted. Several examples are presented in [9], along with a proof that unbounded forwarders are definable in TaskPIOA and hence several important notions of security collapse. Finally, we are able to formulate statistical indistinguishability as an implementation relation in the TaskPIOA framework, which can then be proven using approximate simulation relations [10]. 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 wellknown identification protocol proposed by Girault, Poupard and Stern [11]. References:[1] 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. [2] R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. TaskStructured Probabilistic I/O Automata. In Proceedings of the 8th International Workshop on Discrete Event Systems (WODES'06), July 2006. [3] R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. TaskStructured Probabilistic I/O Automata. Submitted for journal publication. [4] R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Timebounded TaskPIOAs: A Framework for Analyzing Security Protocols''. In Proceedings of the 20th International Symposium on Distributed Computing (DISC 2006), September 2006. [5] R. Canetti, D. Kaynar, M. Liskov, N. Lynch, O. Pereira and R. Segala. Analyzing Security Protocols Using TimeBounded TaskPIOAs. Submitted for journal publication. [6] O. Goldreich, S. Micali, and A. Wigderson. How to play any mental game. Proc. 19th STOC, pp. 218229, 1987. [7] A. Datta, R. Kuesters, J. C. Mitchell, A. Ramanathan. On the Relationship between Notions of SimulationBased Security. In Proceedings of Theory of Cryptography Conference (TCC), 2005. [8] L. Cheung, D. Kaynar, N. Lynch and O. Pereira. Compositional Security for TaskPIOAs. Under review. [9] R. Canetti, L. Cheung, N. Lynch and O. Pereira. On the Role of Scheduling in SimulationBased Security. Accepted at the Workshop on Issues in the Theory of Security (WITS), March 2007. [10] L. Cheung, S. Mitra and O. Pereira. Verifying Statistical Zero Knowledge with Approximate Implementations. Under review. [11] 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):463487, 2006. 

