We present the Time-Bounded Task-PIOA modeling framework, an extension of the Probabilistic I/O Automata (PIOA) framework that is intended to support modeling and verification of security protocols. Time-Bounded Task-PIOAs directly model probabilistic and non-deterministic behavior, partial-information adversarial scheduling, and time-bounded computation. Together, these features are adequate to support modeling of key aspects of security protocols, including secrecy requirements and limitations on the knowledge and computational power of adversarial parties. They also support security protocol verification, using methods that are compatible with informal approaches used in the computational cryptography research community. We illustrate the use of our framework by outlining a proof of functional correctness and security properties for a well-known Oblivious Transfer protocol. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Canetti, R., Cheung, L., Kaynar, D., Liskov, M., Lynch, N., Pereira, O., & Segala, R. (2006). Time-bounded task-PIQAs: A framework for analyzing security protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4167 LNCS, pp. 238–253). Springer Verlag. https://doi.org/10.1007/11864219_17
Mendeley helps you to discover research relevant for your work.