Task-Structured Probabilistic I/O Automata
In the Probabilistic I/O Automata (PIOA) framework, nondeterministicchoices are resolved using perfect-information schedulers,which are similar to history-dependent policies for Markov decision processes(MDPs). These schedulers are too powerful in the setting of securityanalysis, leading to unrealis...
| Main Authors: | , , , , , , |
|---|---|
| Other Authors: | |
| Language: | en_US |
| Published: |
2006
|
| Online Access: | http://hdl.handle.net/1721.1/32525 |
| _version_ | 1811074779471413248 |
|---|---|
| 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 | In the Probabilistic I/O Automata (PIOA) framework, nondeterministicchoices are resolved using perfect-information schedulers,which are similar to history-dependent policies for Markov decision processes(MDPs). These schedulers are too powerful in the setting of securityanalysis, leading to unrealistic adversarial behaviors. Therefore, weintroduce in this paper a novel mechanism of task partitions for PIOAs.This allows us to define partial-information adversaries in a systematicmanner, namely, via sequences of tasks.The resulting task-PIOA framework comes with simple notions of externalbehavior and implementation, and supports simple compositionalityresults. A new type of simulation relation is defined and proven soundwith respect to our notion of implementation. To illustrate the potentialof this framework, we summarize our verification of an ObliviousTransfer protocol, where we combine formal and computational analyses.Finally, we present an extension with extra expressive power, usinglocal schedulers of individual components. |
| first_indexed | 2024-09-23T09:55:22Z |
| id | mit-1721.1/32525 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T09:55:22Z |
| publishDate | 2006 |
| record_format | dspace |
| spelling | mit-1721.1/325252019-04-10T09:59:04Z Task-Structured Probabilistic I/O Automata Canetti, Ran Cheung, Ling Kaynar, Dilsun Liskov, Moses Lynch, Nancy Pereira, Olivier Segala, Roberto Nancy Lynch Theory of Computation In the Probabilistic I/O Automata (PIOA) framework, nondeterministicchoices are resolved using perfect-information schedulers,which are similar to history-dependent policies for Markov decision processes(MDPs). These schedulers are too powerful in the setting of securityanalysis, leading to unrealistic adversarial behaviors. Therefore, weintroduce in this paper a novel mechanism of task partitions for PIOAs.This allows us to define partial-information adversaries in a systematicmanner, namely, via sequences of tasks.The resulting task-PIOA framework comes with simple notions of externalbehavior and implementation, and supports simple compositionalityresults. A new type of simulation relation is defined and proven soundwith respect to our notion of implementation. To illustrate the potentialof this framework, we summarize our verification of an ObliviousTransfer protocol, where we combine formal and computational analyses.Finally, we present an extension with extra expressive power, usinglocal schedulers of individual components. 2006-03-31T17:51:50Z 2006-03-31T17:51:50Z 2006-03-31 MIT-CSAIL-TR-2006-023 http://hdl.handle.net/1721.1/32525 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory http://hdl.handle.net/1721.1/33964 http://hdl.handle.net/1721.1/33964 45 p. 2404679 bytes 487620 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | Canetti, Ran Cheung, Ling Kaynar, Dilsun Liskov, Moses Lynch, Nancy Pereira, Olivier Segala, Roberto Task-Structured Probabilistic I/O Automata |
| title | Task-Structured Probabilistic I/O Automata |
| title_full | Task-Structured Probabilistic I/O Automata |
| title_fullStr | Task-Structured Probabilistic I/O Automata |
| title_full_unstemmed | Task-Structured Probabilistic I/O Automata |
| title_short | Task-Structured Probabilistic I/O Automata |
| title_sort | task structured probabilistic i o automata |
| url | http://hdl.handle.net/1721.1/32525 |
| work_keys_str_mv | AT canettiran taskstructuredprobabilisticioautomata AT cheungling taskstructuredprobabilisticioautomata AT kaynardilsun taskstructuredprobabilisticioautomata AT liskovmoses taskstructuredprobabilisticioautomata AT lynchnancy taskstructuredprobabilisticioautomata AT pereiraolivier taskstructuredprobabilisticioautomata AT segalaroberto taskstructuredprobabilisticioautomata |