Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol
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 analyz...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Published: |
2007
|
| Online Access: | http://hdl.handle.net/1721.1/35918 |
| _version_ | 1811091785577922560 |
|---|---|
| author | Canetti, Ran Cheung, Ling Kaynar, Dilsun Liskov, Moses Lynch, Nancy Pereira, Olivier Segala, Roberto |
| author2 | Nancy Lynch |
| author_facet | Nancy Lynch Canetti, Ran Cheung, Ling Kaynar, Dilsun Liskov, Moses Lynch, Nancy Pereira, Olivier Segala, Roberto |
| author_sort | Canetti, Ran |
| collection | MIT |
| description | 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. |
| first_indexed | 2024-09-23T15:07:59Z |
| id | mit-1721.1/35918 |
| institution | Massachusetts Institute of Technology |
| last_indexed | 2024-09-23T15:07:59Z |
| publishDate | 2007 |
| record_format | dspace |
| spelling | mit-1721.1/359182019-04-12T08:35:53Z Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol Canetti, Ran Cheung, Ling Kaynar, Dilsun Liskov, Moses Lynch, Nancy Pereira, Olivier Segala, Roberto Nancy Lynch Theory of Computation 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. 2007-02-20T13:41:48Z 2007-02-20T13:41:48Z 2007-02-16 MIT-CSAIL-TR-2007-011 http://hdl.handle.net/1721.1/35918 Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory http://hdl.handle.net/1721.1/33217 http://hdl.handle.net/1721.1/33217 98 p. application/pdf application/postscript |
| spellingShingle | Canetti, Ran Cheung, Ling Kaynar, Dilsun Liskov, Moses Lynch, Nancy Pereira, Olivier Segala, Roberto Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol |
| title | Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol |
| title_full | Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol |
| title_fullStr | Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol |
| title_full_unstemmed | Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol |
| title_short | Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol |
| title_sort | using task structured probabilistic i o automata to analyze an oblivious transfer protocol |
| url | http://hdl.handle.net/1721.1/35918 |
| work_keys_str_mv | AT canettiran usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol AT cheungling usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol AT kaynardilsun usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol AT liskovmoses usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol AT lynchnancy usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol AT pereiraolivier usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol AT segalaroberto usingtaskstructuredprobabilisticioautomatatoanalyzeanoblivioustransferprotocol |