Cryptology ePrint Archive: Report 2005/452
Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
Ran Canetti and Ling Cheung and Dilsun Kaynar and Moses Liskov and Nancy Lynch and Olivier Pereira and Roberto Segala
Abstract: The Probabilistic I/O Automata framework of
Lynch, Segala and Vaandrager provides
tools for precisely specifying protocols and reasoning about their
correctness using multiple levels of abstraction, based on
implementation relationships between these levels.
We enhance this framework to allow analyzing
protocols that use cryptographic primitives. This requires resolving and
such as nondeterministic behavior and scheduling, randomness,
resource-bounded computation, and computational hardness assumptions.
The enhanced framework allows for more rigorous and systematic
analysis of cryptographic protocols. To demonstrate the use of this
framework, we present an example analysis that we have done for an
Oblivious Transfer protocol.
Category / Keywords: cyrptographic protocols, oblivious transfer, formal analysis
Date: received 9 Dec 2005, last revised 16 Feb 2007
Contact author: dilsun at cs cmu edu
Available formats: PDF | BibTeX Citation
Note: Improved presentation by making minor changes in automata specifications such as renaming some variables and removing redundant preconditions. Also fixed a bug in the state correspondence (namely Property 1l) used in the simulation relation proof of Section 10.6.
Version: 20070216:165421 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]