Volume 1 - Issue 2 - 3
A Novel Framework for Protocol Analysis
- Kristian Gjøsteen
Norwegian University of Science and Technology, N-7491 Trondheim, Norway
kristiag@math.ntnu.no
- George Petrides
Norwegian University of Science and Technology, N-7491 Trondheim, Norway
petrides@math.ntnu.no
- Asgeir Steine
Norwegian University of Science and Technology, N-7491 Trondheim, Norway
asgeirs@math.ntnu.no
Keywords: Protocol Security, Universal Composability
Abstract
We describe a novel reformulation of Canetti’s Universal Composability (UC) framework for theanalysis of cryptographic protocols. Our framework is different mainly in that it is (a) based onsystems of interactive Turing machines with a fixed communication graph and (b) augmented with aglobal message queue that allows the sending of multiple messages per activation. The first featuresignificantly simplifies the proofs of some framework results, such as the UC theorem, while thesecond can lead to more natural descriptions of protocols and ideal functionalities. We illustrate howthe theory can be used with several examples.