Abstract
Task-structured probabilistic input/output automata (Task-PIOAs) 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 crypto-protocols. We illustrate our approach with an example from anonymity, an area that has not previously been addressed using Task-PIOAs. We model Chaum’s Dining Cryptographers Protocol at a level that does not require cryptographic primitives in the analysis. We show via this example how our approach can leverage a proof of security in the case a principal behaves deterministically to prove security when that principal behaves probabilistically.
The authors wish to thank the Center for Discrete Mathematics and Theoretical Computer Science and the DIMACS Special Focus on Communication Security and Information Privacy for their support that allowed us to gather at Rutgers to work on this project for a week in May/June, 2008.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Gordon, A.: A calculus for cryptographic protocols: The spi calculus. Information and Computation 148, 1–70 (1999)
Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 3, pp. 1–168. Clarendon Press, Oxford (1994)
de Alfaro, L., Henzinger, T., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 351–365. Springer, Heidelberg (2001)
Bhargava, M., Palamidessi, C.: Probabilistic anonymity. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 171–185. Springer, Heidelberg (2005)
Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols, http://eprint.iacr.org/2000/067
Canetti, R., Lynch, N., et al.: Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol (preprint), http://hdl.handle.net/1721.1/33154
Chatzikokolakis, K., Palamidessi, C.: Making Random Choices Invisible to the Scheduler. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 42–58. Springer, Heidelberg (2007)
Chatzikokalakis, K., Palamidessi, C., Panangaden, P.: Anonymity protocols as noisy channels. Information and Computation 206, 378–401 (2008)
Chaum, D.: The dining cryptographers problem: Unconditional sender and recipient untraceability. Journal of Cryptology 1, 65–75 (1988)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Approximating Labeled Markov Processes. Information and Computation 184(1), 160–200 (2003)
Garcia, F., van Rossum, P., Sokolova, A.: Probabilistic anonymity and admissible schedulers, June 2 (2007) arXiv:0706.1019, http://eprintweb.org/S/authors/All/so/Sokolova
Goldreich, O.: Secure Multi-party Computation, http://www.wisdom.weizmann.ac.il/~oded/pp.html
Goldreich, O., Micali, S., Wigderson, A.: Proofs that yield nothing but their validity, or All languages in NP have Zero-knowledge proofs. JACM 38, 691–729 (1991)
Hasuo, I., Kawabe, Y.: Probabilistic anonymity via coalgebraic simulations. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 379–394. Springer, Heidelberg (2007)
Jones, C.: Probabilistic non-determinism. University of Edinburgh, Edinburgh (1992)
Larsen, K.G., Skou, A.: Bisimulation through Probabilistic Testing. Information and Computation 94(1), 1–28 (1991)
Lincoln, Mitchell, P.J.C., Mitchell, M., Scedrov, A.: A Probabilistic Poly-Time Framework for Protocol Analysis. In: ACM Conference on Computer and Communications Security, pp. 112–121 (1998)
Mislove, M.: Nondeterminism and probabilistic choice: obeying the laws. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 350–364. Springer, Heidelberg (2000)
Mislove, M., Pavlovic, D., Worrell, J.: Labelled Markov Processes as Generalized Stochastic Relations. Electronic Notes Theoretical Computer Science, vol. 172, pp. 459–478 (2007)
Mitchell, J., Ramanathan, A., Scedrov, A., Teague, V.: A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols. Theoretical Computer Science 353, 118–164 (2006)
Schneider, S., Sidiropoulos, A.: CSP and anonymity. In: Martella, G., Kurth, H., Montolivo, E., Bertino, E. (eds.) ESORICS 1996. LNCS, vol. 1146, pp. 198–218. Springer, Heidelberg (1996), http://dx.doi.org/10.1007/3-540-61770-1_38
Segala, R.: Modeling and Verification of Randomized Distributed Real-time Systems, PhD Thesis, MIT Technical Report MIT/LCS/TR-676 (1995)
Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. Nordic Journal of Computing 2, 250–273 (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jaggard, A.D., Meadows, C., Mislove, M., Segala, R. (2010). Reasoning about Probabilistic Security Using Task-PIOAs. In: Armando, A., Lowe, G. (eds) Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security. ARSPA-WITS 2010. Lecture Notes in Computer Science, vol 6186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16074-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-16074-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-16073-8
Online ISBN: 978-3-642-16074-5
eBook Packages: Computer ScienceComputer Science (R0)