Reasoning about Probabilistic Security Using Task-PIOAs

Abstract. Task-structured probabilistic input/output automata (taskPIOAs) are concurrent probabilistic automata that, among other things, have been used to provide a formal framework for the universal composability paradigms of protocol security. One of their advantages is that that they allow one to distinguish high-level nondeterminism that can affect the outcome of the protocol, from low-level choices, which can't. We present an alternative approach to analyzing the structure of task-PIOAs that relies on ordered sets. We focus on two of the components that are required to define and apply task-PIOAs: discrete probability theory and automata theory. We believe our development gives insight into the structure of task-PIOAs and how they can be utilized to model cryptoprotocols. We illustrate our approach with an example from anonymity, an area that has not been previously been addressed using task-PIOAs. We model Chaum's Dining Cryptographers protocol at a level that does not...

• Type: Journal
• Year: 2010
• Where: IFIP
• Authors: Aaron D. Jaggard, Catherine Meadows, Michael Mislove, Roberto Segala
• Keywords: Dining Cryptographers Protocol, Discrete Probability Theory, IFIP 2010, Programming Languages, Universal Composability Paradigms