
Research
Abstracts  2006 
TaskStructured Probabilistic I/O AutomataRan Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, & Roberto SegalaIntroductionThe framework of Probabilistic Input/Output Automata (PIOA) is a simple combination of I/O automata [1] and Markov decision processes [2]. As demonstrated in [3,4,5], PIOAs are wellsuited for the analysis of distributed algorithms that use randomness as a computational primitive (see [6]). In this setting, distributed processes use random inputs to improve complexity results for important tasks such as consensus. Thus, each process is modeled as an automaton with randomized transitions, while the 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. First, it provides a convincing option for modeling timing uncertainties in a distributed and highly unpredictable environment. Moreover, it 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). This projects involves an adaptation of the PIOA framework intended for the analysis of cryptographic protocols. These protocols are highly specialized examples of distributed algorithms, designed to protect sensitive data when they are transmitted over unreliable channels. Their correctness typically relies on computational assumptions, which state that certain problems cannot be solved (efficiently) by an adversarial entity with bounded computation resources [7]. The Interactive Turing Machine (ITM) framework can be used to analyze cryptographic protocols on a very detailed level: participants are modeled as ITMs and messages as bit strings written on input tapes [8]. In this setting, complexitytheoretic arguments can be given rigorously, reducing the correctness of a protocol to its underlying cryptographic primitives. However, as protocols become more complex and involve more participants, such finegrained analyses are cluttered by details and thus difficult to carry out. Practical protocols and adversaries are therefore seldom expressed in the language of ITMs. Rather, an informal (and at times ambiguous) higherlevel language is used. We aim to provide a framework in which security analysis can be carried out formally in the style of the ITMbased framework of [8], yet inessential details can be abstracted away in order to facilitate reasoning. Since the PIOA framework allows both nondeterministic and probabilistic choices, finding an appropriate mechanism for resolving nondeterminism is a key issue to be addressed. The standard scheduling mechanism in the cryptographic community is that of an adversarial scheduler, namely, a resourcebounded algorithmic entity that determines the next move to be taken based on the adversarial view of the computation so far. In contrast, the standard in distributed computing is a perfectinformation scheduler, which has access to local state and history of every component and has no limitations on its computation power. The latter is clearly too strong for cryptographic analysis. The main challenge we face is the reconciliation of two different notions of scheduling. ApproachOur solution is a clean separation of concerns. The adaptive adversarial scheduler is modeled explicitly as an automaton, which acts as a message delivery system and thus has access to dynamic information. On the other hand, the remaining nondeterministic choices are resolved by a sequence of tasks that is fixed nondeterministically in advance. These tasks are equivalence classes of action symbols, so that dynamic information is kept independent. We believe this separation is conceptually meaningful. The highlevel adversarial scheduler is responsible for choices that are essential in security analysis, such as the ordering of message deliveries. The lowlevel schedule of tasks resolves inessential choices. ProgressWe defined notions of external behavior and implementation for taskPIOAs , which are PIOAs augmented with task partitions on the set of actions. These notions are based on the trace distribution semantics proposed by Segala [9]. We defined parallel composition in the obvious way and showed that our implementation relation is compositional. A new type of simulation relation, which incorporates the notion of tasks, was also proposed and proven sound. It is very different from simulation relations studied earlier [10,11], in that it is a relation between probability distributions. This definition style is directly motivated by proof techniques in cryptography, where certain probability distributions are deemed ``indistinguishable'' by any resourcebounded entity. The taskPIOA framework has been applied successfully in security analysis [12]. Specifically, it is used to analyze an Oblivious Transfer protocol [13]. That analysis involves a fair amount of additional work, such as definitions of computationally bounded computation, approximate implementation and computational hardness assumptions. Future workAlthough our development is largely motivated by concerns in cryptographic analysis, the notion of partialinformation scheduling is of independent interest. In particular, partialinformation adversaries are widely used to defeat lower bound results proven for perfectinformation adversaries [14,15,16]. We intend to explore applications in this area, possibly extending the present taskPIOA framework. Another good direction to pursue is a full treatment of Canetti's Universal Composability results [8] in terms of taskPIOAs. This will provide a fullfeatured modeling framework for security protocols, which is built upon the rigorous computational foundations of [8] and at the same time inherits the simplicity and modularity of taskPIOAs. Our OT case study confirms that it is indeed possible to carefully separate high and lowlevel nondeterminism. This allows us to use lowlevel nondeterministic choices as a means of abstraction, as commonly done in the verification of noncryptographic algorithms. Finally, we list two technical improvements that are currently under investigation. First, our notion of implementation is currently defined by quantifying over all possible environment automata. We would like to reduce the complexity of this definition by identifying a (minimal) subclass of environments that is sufficient to characterize our implementation relation. Here we may use the idea of principal contexts of [9]. Second, we would like to develop further the notion of local schedulers and evaluate via case studies the tradeoff between expressivity and usability. References[1] N.A. Lynch and M.R. Tuttle. An introduction to input/output automata. CWI Quarterly , 2(3):219246, September 1989. [2] M.L. Puterman. Markov Decision Process  Discrete Stochastic Dynamic Programming . John Wiley and Sons, Inc., New York, NY, 1994. [3] N.A. Lynch, I.Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. In Proc. 13th ACM PODC , pages 314323, 1994. [4] M. Stoelinga and F. Vaandrager. Root contention in {IEEE} 1394. 5th AMAST Formal Methods for RealTime and Prob. Sys. , LNCS 1601, 1999. [5] A.Pogosyants, R.Segala, and N.A. Lynch. Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. Distributed Computing , 13(3):155186, 2000. [6] M. Rabin. The choice coordination problem. Acta Informatica , 17, 1982. [7] O. Goldreich. Foundations of Cryptography: Basic Tools , volume I. Cambridge University Press, 2001. [8] R. Canetti. Universally composable security: a new paradigm for cryptographic protocols. In Proc. 42nd IEEE Symp. on Found. of Comp., 2001. [9] R. Segala. Modeling and Verification of Randomized Distributed RealTime Systems . PhD thesis, EECS, MIT, 1995. Tech. Rep. MIT/LCS/TR676. [10] R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing , 2(2):250273, 1995. [11] N.A. Lynch, R. Segala, and F.W. Vaandrager. Compositionality for probabilistic automata. In {\em Proc. 14th CONCUR} , LNCS 2761, 2003. [12] R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala. Using taskstructured probabilistic I/O automata to analyze an oblivious transfer protocol. Technical Report MITCSAILTR2006019. Extended abstract submitted to CSFW, 2006. [13]O. Goldreich, S. Micali, and A. Wigderson. How to play any mental game. Proc. 19th STOC , pages 218229. ACM, 1987. [14]T.D. Chandra. Polylog randomized waitfree consensus. In Proc. of the 15th ACM Symposium on Principles of Distributed Computing , 1996. [15]J.Aspnes. Randomized protocols for asynchronous consensus. Distributed Computing , 16(23):165175, 2003. [16] Y.Aumann and M.A. Bender. Efficient lowcontention asynchronous consensus with the valueoblivious adversary scheduler. Distributed Computing , 2004. Accepted in 2004. 

