||Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
||Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, Olivier, Roberto Segala
|LCS Document Number:
||Theory of Distributed Systems
|We demonstrate how to carry out cryptographic security analysis of
distributed protocols within the Probabilistic I/O Automata framework
of Lynch, Segala, and Vaandrager.
This framework provides tools for arguing rigorously about the
concurrency and scheduling aspects of protocols, and about protocols
presented at different levels of abstraction.
Consequently, it can help in making cryptographic analysis more
precise and less susceptible to errors.
We concentrate on a relatively simple two-party Oblivious Transfer
protocol, in the presence of a semi-honest adversary (essentially, an
For the underlying cryptographic notion of security, we use a version
of Canetti's Universally Composable security.
In spite of the relative simplicity of the example, the exercise is
It requires taking many fundamental issues into account,
including nondeterministic behavior, scheduling, resource-bounded
computation, and computational hardness assumptions for cryptographic
|To obtain this publication:
To purchase a printed copy of this publication please contact