About the iUC Framework
The iUC framework is an expressive and user friendly universal composability model for the formal security analysis of protocols in a modular way. Universal composability is an important tool for taming the complexity of protocols by allowing for analyzing small parts of a protocol in isolation, which then directly implies security of the combined protocol. The iUC framework provides the so far best combination of expressiveness and ease of use in a universal composability model: it offers modeling conventions, including a template for specifying arbitrary protocols, and comes with a clear and simple syntax as well as sensible default values for many optional parts. At the same time, the iUC framework is highly customizable and includes only very minimal technical requirements, which allows for capturing a wide range of protocols and settings in natural and intuitive ways.
Features of the iUC Framework
The iUC framework provides full and seamless support for, besides others, all of the following:
- All types of protocols considered in the universal composability literature, such as real, ideal, hybrid, joint-state, and global state protocols
- Many interesting protocol features such as:
- flexible protocol structures that allow for connecting individual protocol components in arbitrary ways
- protocols with and without disjoint sessions
- state that can be shared arbitrarily, even across sessions
- locally chosen and/or globally managed session identifiers
- protocols with and without runtime exhaustion
- arbitrary combinations of all of the above
- All composition types from the universal composability literature, including composition of protocols with/without disjoint sessions, composition with joint-state, composition with global state.
- Composition types that have not been considered in the literature so far, such as a new type of joint-state composition for multiple protocols as well as combinations of the above composition types.
All of the above is supported via just a single template and a single main composition theorem, which is in contrast to many other universal composability models and is an important property that makes iUC more user friendly.
The iUC framework was created as an instantiation of the IITM model and published at [AsiaCrypt2019]. The IITM model, published at [CSFW06] with a full and revised version to appear in the Journal of Cryptology (see [eprint13] for the technical report), is a general model for universal composability that was developed by our institute. While the IITM model is very expressive, it, however, does not provide any modeling tools and hence requires some effort to model a protocol. These tools and conventions are added by the iUC framework to create the most expressive yet user friendly universal composability model to date. Both the IITM model and its instantiation the iUC framework have already been used successfully to model and analyze a wide range of protocols in a modular way (see literature below).
Literature and Publications
This work has been supported by Deutsche Forschungsgemeinschaft (DFG).