Task-structured probabilistic I/O automata. (English) Zbl 1390.68382
Summary: Modeling frameworks such as Probabilistic I/O Automata (PIOA) and Markov Decision Processes permit both probabilistic and nondeterministic choices. In order to use these frameworks to express claims about probabilities of events, one needs mechanisms for resolving nondeterministic choices. For PIOAs, nondeterministic choices have traditionally been resolved by schedulers that have perfect information about the past execution. However, these schedulers are too powerful for certain settings, such as cryptographic protocol analysis, where information must sometimes be hidden. In this paper, we propose a new, less powerful nondeterminism-resolution mechanism for PIOAs, consisting of tasks and local schedulers. Tasks are equivalence classes of system actions that are scheduled by oblivious, global task sequences. Local schedulers resolve nondeterminism within system components, based on local information only. The resulting task-PIOA framework yields simple notions of external behavior and implementation, a new kind of simulation relation that is sound for proving implementation, and supports simple compositionality results.
MSC:
| 68Q45 | Formal languages and automata |
| 68Q87 | Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) |
References:
| [1] | Aspnes, J.; Herlihy, M., Fast randomized consensus using shared memory, J. Algorithms, 11, 3, 441-461 (1990) · Zbl 0705.68016 |
| [2] | Archer, M., TAME support for refinement proofs, available at |
| [3] | Aspnes, J., Randomized protocols for asynchronous consensus, Distrib. Comput., 16, 2-3, 165-175 (2003) · Zbl 1448.68063 |
| [4] | Beaver, D., Secure multiparty protocols and zero-knowledge proof systems tolerating a faulty minority, J. Cryptol., 4, 2, 75-122 (1991) · Zbl 0733.68006 |
| [5] | Baier, C.; Kwiatkowska, M., Model checking for a probabilistic branching time logic with fairness, Distrib. Comput., 11, 3, 125-155 (1998) · Zbl 1448.68285 |
| [6] | Ben-Or, M., Another advantage of free choice: completely asynchronous agreement protocols, (Proc. 2nd ACM Symposium on Principles of Distributed Computing. Proc. 2nd ACM Symposium on Principles of Distributed Computing, Montreal, Quebec, Canada (August 1983)), 27-30 |
| [7] | Backes, M.; Pfitzmann, B.; Waidner, M., The reactive simulatability (RSIM) framework for asynchronous systems, Inf. Comput., 205, 12, 1685-1720 (December 2007) · Zbl 1132.68025 |
| [8] | Canetti, R., Studies in Secure Multi-Party Computation and Applications (1995), Weizmann Institute: Weizmann Institute Israel, PhD thesis |
| [9] | Canetti, R., Universally composable security: a new paradigm for cryptographic protocols, (Proc. 42nd IEEE Symposium on Foundations of Computing (2001)), 136-145 |
| [10] | Canetti, R.; Cheung, L.; Kaynar, D.; Liskov, M.; Lynch, N.; Pereira, O.; Segala, R., Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol (2005), MIT CSAIL, Technical Report MIT-LCS-TR-1001a or MIT-CSAIL-TR-2005-055 |
| [11] | Canetti, R.; Cheung, L.; Kaynar, D.; Liskov, M.; Lynch, N.; Pereira, O.; Segala, R., Using Task-Structured Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol (2005), available at |
| [12] | Canetti, R.; Cheung, L.; Kaynar, D.; Liskov, M.; Lynch, N.; Pereira, O.; Segala, R., Task-Structured Probabilistic I/O Automata (2006), MIT CSAIL, Technical Report MIT-CSAIL-TR-2006-023 |
| [13] | Canetti, R.; Cheung, L.; Kaynar, D.; Liskov, M.; Lynch, N.; Pereira, O.; Segala, R., Task-structured probabilistic I/O automata, (Proceedings of the 8th International Workshop on Discrete Event Systems. Proceedings of the 8th International Workshop on Discrete Event Systems, WODES’06, Ann Arbor, Michigan, 2006 (July 2006)) |
| [14] | Canetti, R.; Cheung, L.; Kaynar, D.; Liskov, M.; Lynch, N.; Pereira, O.; Segala, R., Time-bounded task-PIOAs: a framework for analyzing security protocols, (Proceedings of the 20th International Symposium on Distributed Computing. Proceedings of the 20th International Symposium on Distributed Computing, DISC ’06, Stockholm, Sweden, 2006 (September 2006)) · Zbl 1155.68326 |
| [15] | Canetti, R.; Cheung, L.; Kaynar, D.; Lynch, N.; Pereira, Olivier, Compositional security for Task-PIOAs, (Proceedings of the 20th IEEE Computer Security Foundations Symposium. Proceedings of the 20th IEEE Computer Security Foundations Symposium, CSF-20 (July 2007), IEEE Computer Society Press), 125-139 |
| [16] | Canetti, R.; Cheung, L.; Lynch, N.; Pereira, O., On the role of scheduling in simulation-based security, (Focardi, R., Proceedings of the 7th International Workshop on Issues in the Theory of Security. Proceedings of the 7th International Workshop on Issues in the Theory of Security, WITS ’07 (March 2007)), 22-37, available at |
| [17] | Cheung, L.; Hendriks, M., Causal Dependencies in Parallel Composition of Stochastic Processes (2005), Institute for Computing and Information Sciences, University of Nijmegen, Technical Report ICIS-R05020 |
| [18] | Chandra, T. D., Polylog randomized wait-free consensus, (Proc. 15th ACM Symposium on Principles of Distributed Computing (1996)), 166-175 · Zbl 1321.68066 |
| [19] | Canetti, R.; Cheung, L.; Kaynar, D.; Liskov, M.; Lynch, N.; Pereira, O.; Segala, R., Using task-structured probabilistic I/O automata to analyze cryptographic protocol, (Cortier, V.; Kremer, S., Proceedings of Workshop on Formal and Computational Cryptography. Proceedings of Workshop on Formal and Computational Cryptography, FCC ’06 (2006)), 34-39 |
| [20] | Cheung, L.; Lynch, N.; Segala, R.; Vaandrager, F., Switched PIOA: parallel composition via distributed scheduling, Theor. Comput. Sci., 365, 1-2, 83-108 (2006) · Zbl 1118.68038 |
| [21] | Cheung, Ling; Mitra, Sayan; Pereira, Olivier, Verifying Statistical Zero Knowledge with Approximate Implementations (2007), available at |
| [22] | de Alfaro, L., The verification of probabilistic systems under memoryless partial-information policies is hard, (Proc. PROBMIV 99 (1999)), 19-32 |
| [23] | Derman, C., Finite State Markovian Decision Processes (1970), Academic Press · Zbl 0262.90001 |
| [24] | Datta, A.; Küsters, R.; Mitchell, J. C.; Ramanathan, A., On the relationships between notions of simulation-based security, (Proceedings TCC 2005 (2005)), 476-494 · Zbl 1079.94543 |
| [25] | Goldwasser, S.; Levin, L., Fair computation of general functions in presence of immoral majority, (Menezes, Alfred J.; Vanstone, Scott A., Advances in Cryptology. Advances in Cryptology, Crypto ’90. Advances in Cryptology. Advances in Cryptology, Crypto ’90, Lecture Notes in Computer Science, vol. 537 (1990), Springer-Verlag: Springer-Verlag Berlin), 77-93 · Zbl 0800.68459 |
| [26] | Goldwasser, S.; Micali, S.; Rackoff, C., The knowledge complexity of interactive proof systems, (Proceedings of the 17th Annual ACM Symposium on Theory of Computing. Proceedings of the 17th Annual ACM Symposium on Theory of Computing, STOC’85 (1985)), 291-304 · Zbl 0900.94025 |
| [27] | Goldreich, O.; Micali, S.; Wigderson, A., How to play any mental game, (Proc. 19th ACM Symposium on Theory of Computing. Proc. 19th ACM Symposium on Theory of Computing, STOC (1987)), 218-229 |
| [28] | Girault, Marc; Poupard, Guillaume; Stern, Jacques, On the fly authentication and signature schemes based on groups of unknown order, J. Cryptol., 19, 4, 463-487 (2006) · Zbl 1133.94345 |
| [29] | Jonsson, B.; Larsen, K. G., Specification and refinement of probabilistic processes, (Proceedings of the 6th IEEE Symposium on Logic in Computer Science (1991)), 266-277 |
| [30] | Kantorovitch, L., On the translocation of masses, Manag. Sci., 5, 1, 1-4 (1958) · Zbl 0995.90585 |
| [31] | Kaelbling, L. P.; Littman, M. L.; Cassandra, A. R., Planning and acting in partially observable stochastic domains, Artif. Intell., 101, 99-134 (1998) · Zbl 0908.68165 |
| [32] | Lincoln, P.; Mitchell, J. C.; Mitchell, M.; Scedrov, A., A probabilistic poly-time framework for protocol analysis, (ACM Conference on Computer and Communications Security (1998)), 112-121 |
| [33] | Lynch, N. A.; Saias, I.; Segala, R., Proving time bounds for randomized distributed algorithms, (Proc. 13th ACM Symposium on the Principles of Distributed Computing (1994)), 314-323 · Zbl 1373.68448 |
| [34] | Lynch, N. A.; Segala, R.; Vaandrager, F. W., Compositionality for probabilistic automata, (Proc. 14th International Conference on Concurrency Theory. Proc. 14th International Conference on Concurrency Theory, CONCUR 2003. Proc. 14th International Conference on Concurrency Theory. Proc. 14th International Conference on Concurrency Theory, CONCUR 2003, LNCS, vol. 2761 (2003), Springer-Verlag), 208-221 · Zbl 1274.68161 |
| [35] | Lynch, N. A.; Segala, R.; Vaandrager, F. W., Observing branching structure through probabilistic contexts, SIAM J. Comput., 37, 977-1013 (2007) · Zbl 1156.68020 |
| [36] | Lynch, N. A.; Tuttle, M. R., An introduction to input/output automata, Quart. - Cent. Wiskd. Inform., 2, 3, 219-246 (September 1989) · Zbl 0677.68067 |
| [37] | Mitra, S.; Lynch, N. A., Probabilistic timed I/O automata with continuous state spaces (May 2006), preliminary version available at |
| [38] | Mitra, Sayan; Lynch, Nancy, Approximate implementation relations for probabilistic I/O automata, Electron. Notes Theor. Comput. Sci., 174, 8, 71-93 (2007) · Zbl 1277.68111 |
| [39] | Mateus, P.; Mitchell, J. C.; Scedrov, A., Composition of cryptographic protocols in a probabilistic polynomial-time process calculus, (Proc. 14th International Conference on Concurrency Theory. Proc. 14th International Conference on Concurrency Theory, CONCUR 2003 (2003)), 323-345 · Zbl 1274.94097 |
| [40] | Micali, S.; Rogaway, P., Secure computation, (Feigenbaum, Joan, Advances in Cryptology. Advances in Cryptology, Crypto ’91. Advances in Cryptology. Advances in Cryptology, Crypto ’91, Lecture Notes in Computer Science, vol. 576 (1991), Springer-Verlag: Springer-Verlag Berlin), 392-404 |
| [41] | Mitchell, J.; Ramanathan, A.; Scedrov, A.; Teague, V., A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols, Theor. Comput. Sci., 353, 118-164 (2006) · Zbl 1088.68126 |
| [42] | Nagao, Waka; Manabe, Yoshifumi; Okamoto, Tatsuaki, Relationship of three cryptographic channels in the UC framework, (Provable Security, Second International Conference. Provable Security, Second International Conference, ProvSec 2008. Provable Security, Second International Conference. Provable Security, Second International Conference, ProvSec 2008, LNCS, vol. 5324 (2008), Springer), 268-282 · Zbl 1204.94076 |
| [43] | Pogosyants, A.; Segala, R.; Lynch, N. A., Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study, Distrib. Comput., 13, 3, 155-186 (2000) · Zbl 1448.68156 |
| [44] | Puterman, M. L., Markov Decision Process - Discrete Stochastic Dynamic Programming (1994), John Wiley & Sons, Inc.: John Wiley & Sons, Inc. New York, NY · Zbl 0829.90134 |
| [45] | Pfitzmann, Birgit; Waidner, Michael, A General Framework for Formal Notions of “Secure” System (April 1994), Institut für Informatik, Universität Hildesheim, Technical Report, Hildesheimer Informatik-Berichte 11/94 |
| [46] | Pfitzman, B.; Waidner, M., Composition and integrity preservation of secure reactive systems, (Proc. 7th ACM Conference on Computer and Communications Security. Proc. 7th ACM Conference on Computer and Communications Security, CCS 2000 (2000)), 245-254 |
| [47] | Pfitzman, B.; Waidner, M., A model for asynchronous reactive systems and its application to secure message transmission, (Proc. IEEE Symposium on Research in Security and Privacy (2001)), 184-200 |
| [48] | Rabin, M., The choice coordination problem, Acta Inform., 17, 121-134 (1982) · Zbl 0479.68048 |
| [49] | Sokolova, A.; de Vink, E. P., Probabilistic automata: system types, parallel composition and comparison, (Validation of Stochastic Systems. Validation of Stochastic Systems, LNCS, vol. 2925 (2004), Springer-Verlag), 1-43 · Zbl 1203.68089 |
| [50] | Segala, R., Modeling and Verification of Randomized Distributed Real-Time Systems (June 1995), Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, available as Technical Report MIT/LCS/TR-676 |
| [51] | Segala, R.; Lynch, N. A., Probabilistic simulations for probabilistic processes, Nord. J. Comput., 2, 2, 250-273 (1995) · Zbl 0839.68067 |
| [52] | Stoelinga, M. I.A.; Vaandrager, F. W., Root contention in IEEE 1394, (Proc. 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems. Proc. 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, LNCS, vol. 1601 (1999), Springer-Verlag), 53-74 |
| [53] | TAME Tempo Toolset, available at |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
