Jan Camenisch, Stephan Krenn, Ralf Küsters, and Daniel Rausch
Proving the security of complex protocols is a crucial and very challenging task. A widely used ap- proach for reasoning about such protocols in a modular way is universal composability. Several models for this approach exist, including the UC, GNUC, and IITM models. Despite the wide spread use of the universal composability approach, none of the existing models are fully satisfying. They all lack either soundness, flexibility, or usability. As a result, proofs in the litera- ture are very often formally incorrect, protocols cannot be modeled faithfully, and/or using these models is a burden rather than a help. Given this dire state of affairs, the goal of this work is to provide a framework for universal composability which combines soundness, flexibility, and usability. Developing such a security framework is a very difficult and delicate task, as the long history of frameworks for universal composability shows. As the IITM model appears to be closest to this goal in terms of soundness and flexibility, we build our framework, called iUC, on top of the IITM model. At the core of iUC is a single simple template for spec- ifying essentially arbitrary protocols in a convenient, formally precise, and flexible way, which allows protocol designers to concentrate on the core logic of a protocol. We illustrate the main features of our framework with example functionalities and realizations.