A Novel Framework for Protocol Analysis

Kristian Gjøsteen, George Petrides and Asgeir Steine

Norwegian University of Science and Technology

N-7491 Trondheim, Norway

{kristiag,petrides,sgeirs}@math.ntnu.no

Abstract

We describe a novel reformulation of Canetti’s Universal Composability (UC) framework for the

analysis of cryptographic protocols. Our framework is different mainly in that it is (a) based on

systems of interactive Turing machines with a fixed communication graph and (b) augmented with a

global message queue that allows the sending of multiple messages per activation. The first feature

significantly simplifies the proofs of some framework results, such as the UC theorem, while the

second can lead to more natural descriptions of protocols and ideal functionalities. We illustrate how

the theory can be used with several examples.

Keywords: Protocol Security, Universal Composability