Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols

Appears: Proceedings of the 20th International Symposium on Distributed Computing (DISC '06), Stockholm, Sweden, LNCS 4167, pages 238-253, September 2006.

Abstract: 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 veri.cation of security protocols. Time-Bounded Task-PIOAs directly model probabilistic and nondeterministic 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 veri.cation, 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.

Download the paper from the publisher.

Download an author-prepared copy of the paper (© Springer-Verlag).