Skip to Main content Skip to Navigation
Conference papers

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

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Véronique Cortier <>
Submitted on : Tuesday, June 20, 2006 - 3:00:27 PM
Last modification on : Tuesday, December 8, 2020 - 3:24:22 PM
Long-term archiving on: : Monday, April 5, 2010 - 11:07:14 PM


  • HAL Id : inria-00080681, version 1



Ran Canetti, Ling Cheung, Dilsun Kaynar, Moses Liskov, Nancy Lynch, et al.. Using Task-Structured Probabilistic I/O Automata to Analyze Cryptographic Protocols. Workshop on Formal and Computational Cryptography (FCC 2006), Véronique Cortier et Steve Kremer, Jul 2006, Venice/Italy. ⟨inria-00080681⟩



Record views


Files downloads