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.