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

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

Paper 2005/452

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

Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, 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 reconciling issues 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.

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.

Metadata

Available format(s): PDF
Publication info: Published elsewhere. Unknown where it was published
Keywords: cyrptographic protocols oblivious transfer formal analysis
Contact author(s): dilsun @ cs cmu edu
History: 2007-02-16: last of 3 revisions; 2005-12-14: received; See all versions
Short URL: https://ia.cr/2005/452
License: CC BY

BibTeX

@misc{cryptoeprint:2005/452,
      author = {Ran Canetti and Ling Cheung and Dilsun Kaynar and Moses Liskov and Nancy Lynch and Olivier Pereira and Roberto Segala},
      title = {Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol},
      howpublished = {Cryptology {ePrint} Archive, Paper 2005/452},
      year = {2005},
      url = {https://eprint.iacr.org/2005/452}
}