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

Appears: Proceedings of the Workshop on Formal and Computational Cryptography (FCC '06), pages 34--39, July 2006.

Abstract: 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 relationships 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 hardness assumptions, and for proving security in a composable setting.