Composable Security Modelling for Practical Protocols
Jan Camenisch
Abstract:
Proving the security of complex protocols is a crucial and very challenging task. We want to design and analyze protocols in a modular way by combining idealized components that we realize individually. A widely used approach for reasoning about such protocols in a modular way is universal composability. In this talk we are going to consider two aspects where widely used frameworks fall short and propose means to address them.
The first issue is that when analysing practical protocols, one is often forced to resort to less efficient designs. For instance, the natural protocol to prove in zero-knowledge knowledge of a signature on a committed value cannot be proved secure in Canetti’s UC framework because of limitations of its composition theorem. We will discuss what goes wrong and propose a multi-protocol composition theorem that solves the problem and a thus allows one to prove secure a wide range of practical protocols which previously could only be analysed in a monolithic manner.
The second issue we discuss is the usability of widely used security composition frameworks. While many such frameworks exist, none of them is flexible enough to allow for the modelling of a multitude of different protocols and different setting. In the second half of the talk we will introduce iUC which is a instantiation of Kuester’s IITM. At the core of iUC is one convenient template that supports protocol designers in specifying arbitrary types of protocols in a precise, intuitive, and compact way. This is made possible by new concepts, including the concept of entities as well as public and private roles. The template comes with a clear and intuitive syntax which further facilitates specifications and allows others to quickly pick up protocol specifications and use them as subroutines in their higher-level protocols.