Using Probabilistic I/O Automata to Analyze an Oblivious Transfer
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch,
Olivier Pereira, Roberto Segala & Frits Vaandrager
Modeling cryptographic protocols and analyzing their security is a tricky
business. On the one hand, valid modeling and analysis has to address
the concurrency aspects of asynchronous distributed systems, with potentially
adversarial scheduling of events. On the other hand, realistic analysis
has to accommodate the fact that, in most interesting cases, it is impossible
to completely prevent successful attacks against the protocol. Instead,
we can only bound the success probability of attacks that use a bounded
amount of computational resources, based on underlying computational hardness
Cryptographic modeling and analysis is typically complex, involving
many subtleties and details, even when the analyzed protocols are simple.
Furthermore, analysis is handwritten and often tedious to verify. These
factors make security analysis of cryptographic protocols susceptible
to errors and omissions.
This project demonstrates how to cast cryptographic security analysis
of distributed protocols within the Probabilistic I/O Automata framework
of Lynch, Segala, and Vaandrager . This framework
provides standard tools for arguing rigorously about the concurrency and
scheduling aspects of protocols. It supports reasoning with multiple levels
of abstraction and has a well-defined notion of composition. Consequently,
using the PIOA framework can help in making cryptographic analysis more
precise and less susceptible to errors.
In the context of this project, we aim to develop general techniques
applicable to the analysis of a wide range of security protocols that
exhibit various levels of complexity in terms of adversarial behavior
or the use of cryptographic primitives. As a first step, we are currently
analyzing a relatively simple protocol, two-party Oblivious Transfer protocol,
in the presence of a semi-honest adversary (essentially, an eavesdropper).
The particular OT protocol we analyze is the classic protocol of
, which uses trapdoor permutations (and hard-core predicates for
them) as the underlying cryptographic primitive. For the underlying cryptographic
notion of security, we start from Canetti's Universally Composable Security
In spite of the relative simplicity of the investigated case, the exercise
is nontrivial and requires addressing fundamental issues such as modeling
resource bounded-computations, resource-bounded adversarial behavior and
scheduling, combining nondeterministic and probabilistic choices, and
modeling computational hardness assumptions some of which are beyond the
reach of the existing semantic theory of probabilistic I/O automata. Therefore,
this project involves not only using the probabilistic I/O automata of
 in security protocol analysis but also extending
the basic theory to address the requirements of such analysis.
One common approach to simplifying cryptographic protocol analysis and
improving its correctness is to model cryptographic primitives as ``symbolic
operations'', or ``ideal boxes'', which represent the security properties
of the primitives in an idealized way that involves no error probabilities
or computational issues. This approach is quite promising; however, it
does not completely remove the need for cryptographic analysis of protocols.
Rather, it only proves security of the overall protocol assuming security
of the cryptographic primitives in use. One still has to prove security
of these primitives in a full-fledged cryptographic model with all its
subtleties. Our project proposes an alternative (in fact, complementary)
approach to making cryptographic protocol analysis more systematic and
rigorous, and thus less susceptible to errors.
We benefit from the powerful proof techniques that have traditionally
been used within I/O automaton frameworks. In particular, we express the
system at multiple levels of abstraction where the highest level in the
abstraction hierarchy represents the specification of the protocol and
the lowest level represents the real-world system running the protocol.
We demonstrate simulation relations between these levels that allow us
to conclude that the real-world system implements the abstract specification.
The composition operation for PIOAs makes it possible to separate the
specification of correctness and security requirements of the protocol,
and to express the real-world system naturally, as a composition of logically
separate units interacting with another.
We have successfully modeled the protocol using probabilistic I/O automata
of  and have layed out our method for analysis. We
have also specified the automata that appear in intermediate levels of
abstraction in showing that the given protocol securely-realizes its specification
in the sense of . The cryptographic primitives are
used only at these intermediate levels so that reasoning about resource-bounded
computations and computational hardness assumptions can be isolated to
those cases of the proof that involve these intermediate levels.
We have defined a special class of PIOAs, called task-PIOAs, that admit
a simple scheduling mechanism and new notions of implementation relations
and simulation relations for task-PIOAs that make our analysis more manageable.
Furthermore, we extended our new theory to capture time-bounded computations
We are in the process of proving the implementation relationships between
levels in our automaton hierarchy, using the appropriate notions of simulation
relations and invariants, and composition theorems.
We would like to assess the techniques we have developed so far in the
analysis of more complex protocols. This complexity may be due more powerful
adversaries, more complex interaction patterns between the components
of the protocol, or more subtle uses of cryptographic primitives.
One limitation of our current approach is that the existing scheduling
mechanism is oblivious to execution histories and, hence, limits the capabilities
of the adversarial components significantly. We will investigate how our
assumptions about task-PIOAs and scheduling mechanisms can be relaxed
to enable the analysis of a larger class of protocols.
Once our modeling and proof techniques become more general and established,
we can focus on mechanizing our proofs with interactive theorem-provers,
or even automating some or all proof steps.
This project is supported by DARPA Air Force contract number FA9550-04-C-0084,
DARPA Award number F33615-01-C-1896, NSF Award numbers CCR-0326277 and
CCR-0121277, NSF-Texas Engineering Experiment Station grant 64961-CS,
DARPA/AFOSR MURI Award F49620-02-1-0325 and MURI AFOSR Award Number SA2796PO
 Nancy Lynch, Roberto Segala, and Frits Vaandrager.
Compositionality for Probabilistic Automata. In Roberto Amadio and
Denis Lugiez, editors, CONCUR 2003 - Concurrency Theory (14th International
Conference on Concurrency Theory, Marseille, France, September, 2003)
, volume 2761 of Lecture Notes in Computer Science, pages 208-221,
Springer-Verlag, 2003. Also, long version to appear as Technical Report
MIT-LCS-TR-907, MIT Laboratory for Computer Science, Cambridge, MA 02139.
 S. Even, O. Goldreich and A. Lempel, A randomized
protocol for signing contracts, CACM vol. 28, No. 6, 1985,
 Ran Canetti. Universally composable security: A
new paradigm for cryptographic protocols. Available at http://eprint.iacr.org/2000/067.
Extended abstract in 42nd FOCS, 2001.