Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol

We demonstrate how to carry out cryptographic security analysis ofdistributed protocols within the Probabilistic I/O Automata frameworkof Lynch, Segala, and Vaandrager.This framework provides tools for arguing rigorously about theconcurrency and scheduling aspects of protocols, and about protocolspresented at different levels of abstraction.Consequently, it can help in making cryptographic analysis moreprecise and less susceptible to errors.We concentrate on a relatively simple two-party Oblivious Transferprotocol, in the presence of a semi-honest adversary (essentially, aneavesdropper).For the underlying cryptographic notion of security, we use a versionof Canetti's Universally Composable security.In spite of the relative simplicity of the example, the exercise isquite nontrivial.It requires taking many fundamental issues into account,including nondeterministic behavior, scheduling, resource-boundedcomputation, and computational hardness assumptions for cryptographicprimitives