Research Abstracts - 2006

Task-Structured Probabilistic I/O Automata

Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier Pereira, & Roberto Segala

Introduction

The 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 well-suited 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, complexity-theoretic 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 fine-grained 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) higher-level language is used. We aim to provide a framework in which security analysis can be carried out formally in the style of the ITM-based 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 resource-bounded 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 perfect-information 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.

Approach

Our 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 high-level adversarial scheduler is responsible for choices that are essential in security analysis, such as the ordering of message deliveries. The low-level schedule of tasks resolves inessential choices.

Progress

We defined notions of external behavior and implementation for task-PIOAs , 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 resource-bounded entity. The task-PIOA 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 work

Although our development is largely motivated by concerns in cryptographic analysis, the notion of partial-information scheduling is of independent interest. In particular, partial-information adversaries are widely used to defeat lower bound results proven for perfect-information adversaries [14,15,16]. We intend to explore applications in this area, possibly extending the present task-PIOA framework.

Another good direction to pursue is a full treatment of Canetti's Universal Composability results [8] in terms of task-PIOAs. This will provide a full-featured 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 task-PIOAs. Our OT case study confirms that it is indeed possible to carefully separate high- and low-level nondeterminism. This allows us to use low-level nondeterministic choices as a means of abstraction, as commonly done in the verification of non-cryptographic 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):219--246, 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 314--323, 1994.

[4] M. Stoelinga and F. Vaandrager. Root contention in {IEEE} 1394. 5th AMAST Formal Methods for Real-Time 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):155--186, 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 Real-Time Systems . PhD thesis, EECS, MIT, 1995. Tech. Rep. MIT/LCS/TR-676.

[10] R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing , 2(2):250--273, 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 task-structured probabilistic I/O automata to analyze an oblivious transfer protocol. Technical Report MIT-CSAIL-TR-2006-019. Extended abstract submitted to CSFW, 2006.

[13]O. Goldreich, S. Micali, and A. Wigderson. How to play any mental game. Proc. 19th STOC , pages 218--229. ACM, 1987.

[14]T.D. Chandra. Polylog randomized wait-free 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(2-3):165--175, 2003.

[16] Y.Aumann and M.A. Bender. Efficient low-contention asynchronous consensus with the value-oblivious adversary scheduler. Distributed Computing , 2004. Accepted in 2004.