- Link:
- http://hdl.handle.net/1721.1/32525
- Collection:
-
- Creators:
- Liskov, Moses Pereira, Olivier Cheung, Ling Lynch, Nancy Canetti, Ran Kaynar, Dilsun Segala, Roberto
- Contributors:
- Theory of Computation Nancy Lynch
- Format
- 45 p.
- Format
- 2404679 bytes
- Format
- 487620 bytes
- Format
- application/postscript
- Format
- application/pdf
- Language
- en_US
- Relation
- Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory
- Relation
- http://hdl.handle.net/1721.1/33964
- 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.
- Relation
- Massachusetts Institute of Technology Computer Science
and Artificial Intelligence Laboratory
- Visits:
- 1
- Access:
- Instructions in case access is denied
Site powered by:
