Using task-structured probabilistic I/O automata to analyze cryptographic protocols
Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses D. Liskov, Nancy Ann Lynch, Olivier Pereira, Roberto Segala · HAL (Le Centre pour la Communication Scientifique Directe) · 2006
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.