iUC: Flexible Universal Composability Made Simple
iUC: Flexible Universal Composability Made Simple
复制标题
DOI：
10.1007/978-3-030-34618-8_7
复制
发表时间：
2019-12
期刊：
影响因子：
--
通讯作者：
J. Camenisch;S. Krenn;Ralf Küsters;Daniel Rausch
中科院分区：
文献类型：
--
作者：
J. Camenisch;S. Krenn;Ralf Küsters;Daniel Rausch
证明复杂协议的安全性是一项至关重要且极具挑战性的任务。以模块化方式推理此类协议的一种广泛使用的方法是通用可组合性。通用可组合性的完美模型应该为形式证明提供可靠的基础，并且非常灵活，以便允许对大量不同的协议进行建模。它还应该易于使用，包括用于重复建模方面的有用设计约定，例如损坏、各方、会话和子例程关系，以便协议设计人员可以专注于其协议的核心逻辑。尽管存在许多通用可组合性模型，包括UC、GNUC和IITM模型，但还没有一个实现这一理想目标。因此，协议不能被准确地建模和/或使用这些模型是负担而不是帮助，甚至经常导致协议描述不足和形式上不正确的证明。鉴于这种可怕的情况，本工作的目标是提供一个以无与伦比的方式结合可靠性、灵活性和可用性的通用可组合性框架。开发这样一个安全框架是一项非常困难和微妙的任务，正如通用可组合性框架的悠久历史所表明的那样。我们在IITM模型的基础上构建了我们的框架IUC，该模型已经提供了可靠性和灵活性，但缺乏足够的可用性。IUC的核心是一个简单的模板，用于以方便、形式精确和灵活的方式指定基本上任意的协议。我们用实例功能和实现来说明我们框架的主要特征。
Proving the security of complex protocols is a crucial and very challenging task. A widely used approach for reasoning about such protocols in a modular way is universal composability. A perfect model for universal composability should provide a sound basis for formal proofs and be very flexible in order to allow for modeling a multitude of different protocols. It should also be easy to use, including useful design conventions for repetitive modeling aspects, such as corruption, parties, sessions, and subroutine relationships, such that protocol designers can focus on the core logic of their protocols.While many models for universal composability exist, including the UC, GNUC, and IITM models, none of them has achieved this ideal goal yet. As a result, protocols cannot be modeled faithfully and/or using these models is a burden rather than a help, often even leading to underspecified protocols and formally incorrect proofs.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 in an unmatched way. Developing such a security framework is a very difficult and delicate task, as the long history of frameworks for universal composability shows.We build our framework, called iUC, on top of the IITM model, which already provides soundness and flexibility while lacking sufficient usability. At the core of iUC is a single simple template for specifying essentially arbitrary protocols in a convenient, formally precise, and flexible way. We illustrate the main features of our framework with example functionalities and realizations.