Modeling Computational Security in Long-Lived Systems, Version 2
Ran Canetti, Ling Cheung, et al.
Dagstuhl Seminar Proceedings 2008
This paper presents the time-bounded task-PIOA modeling framework, an extension of the probabilistic input/output automata (PIOA) framework that can be used for modeling and verifying security protocols. Time-bounded task-PIOAs can describe probabilistic and nondeterministic behavior, as well as time-bounded computation. Together, these features support modeling of important aspects of security protocols, including secrecy requirements and limitations on the computational power of adversarial parties. They also support security protocol verification using methods that are compatible with less formal 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. © 2007 Springer Science+Business Media, LLC.
Ran Canetti, Ling Cheung, et al.
Dagstuhl Seminar Proceedings 2008
Boaz Barak, Ran Canetti, et al.
Journal of Cryptology
Ran Canetti, Ling Cheung, et al.
WODES 2006
Ran Canetti, Ling Cheung, et al.
WODES 2006