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 protocolverification 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.
Time-Bounded Task-PIOAs: A Framework for Analyzing Security Protocols
SEGALA, Roberto
2006-01-01
Abstract
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 protocolverification 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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
