Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols

The Probabilistic I/O Automata (PIOA) framework of Lynch, Segala and Vaandrager provides tools for precisely specifying protocols and reasoning about their correctness based on implementation relation- ships between multiple levels of abstraction. We enhance this framework to allow the analysis of protocols that use cryptographic primitives. For this purpose, we propose new techniques for handling nondeterministic behaviors, expressing computationally hard- ness assumptions, and for proving security in a composable setting.