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 theircorrectness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyz...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2006
|
| Online Access: | http://hdl.handle.net/1721.1/33217 |
| _version_ | 1811097058257403904 |
|---|---|
| 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 theircorrectness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyzingprotocols that use cryptographic primitives. This requires resolving andreconciling 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-23T16:53:40Z |
| id | mit-1721.1/33217 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T16:53:40Z |
| publishDate | 2006 |
| record_format | dspace |
| spelling | mit-1721.1/332172019-04-12T08:35:55Z 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 theircorrectness using multiple levels of abstraction, based on implementation relationships between these levels. We enhance this framework to allow analyzingprotocols that use cryptographic primitives. This requires resolving andreconciling 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. 2006-06-20T21:18:08Z 2006-06-20T21:18:08Z 2006-06-20 MIT-CSAIL-TR-2006-047 http://hdl.handle.net/1721.1/33217 June 19, 2006 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory http://hdl.handle.net/1721.1/31310 http://hdl.handle.net/1721.1/35918 http://hdl.handle.net/1721.1/35918 http://hdl.handle.net/1721.1/31310 98 p. 898579 bytes 5581045 bytes application/pdf application/postscript 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/33217 |
| 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 |