IEEE Symposium on Security and Privacy (S&P)

AUC: Accountable Universal Composability

Mike Graf, Ralf Küsters, Daniel Rausch

Published May 1, 2023• 6 citations

Abstract

Accountability is a well-established and widely used security concept that allows for obtaining undeniable cryptographic proof of misbehavior, thereby incentivizing honest behavior. There already exist several general purpose account-ability frameworks for formal game-based security analyses. Unfortunately, such game-based frameworks do not support modular security analyses, which is an important tool to handle the complexity of modern protocols.Universal composability (UC) models provide native support for modular analyses, including re-use and composition of security results. So far, accountability has mainly been modeled and analyzed in UC models for the special case of MPC protocols, with a general purpose accountability framework for UC still missing. That is, a framework that among others supports arbitrary protocols, a wide range of accountability properties, handling and mixing of accountable and non-accountable security properties, and modular analysis of accountable protocols.To close this gap, we propose AUC, the first general purpose accountability framework for UC models, which supports all of the above, based on several new concepts. We exemplify AUC in three case studies not covered by existing works. In particular, AUC unifies existing UC accountability approaches within a single framework.

DOI: 10.1109/sp46215.2023.10179384

Related papers

Can universally composable cryptographic protocols be practical?

István Vajda

The Universal Composability (UC) framework provides provable security guaranties for harsh application environment, where we want to construct protocols which keep security guarantees even when they are concurrently composed with arbitrary number of arbitrary (even hostile) protocols.This is a very strong guarantee.The UC-framework inherently supports the modular design, which allows secure composition of arbitrary number of UC-secure components with an arbitrary protocol.In contrast, traditional analysis and design is a stand alone analysis where security of a single instance is considered, i.e. an instance which is not in potential interaction with any concurrent instances.Furthermore, a typical traditional analysis is informal, i.e. without a formal proof.In spite of these facts, beyond the task of key-exchange this technology have not really took the attention of the community of applied cryptography.From practitioner's point of view the UC-world may seem more or less an academic interest of theoretical cryptographers.Accordingly we take a pragmatic approach, where we concentrate on meaningful compromises between the assumed adversarial strength, ideality wishes and realization complexity while keeping provable security guarantees within the UC-framework.We believe that even modest but provable goals (especially, if tunable to application scenarios) are interesting if a wider penetration of the UC-technology is desired into the daily-practice of protocol applications.

International Journal of Computer Network and Information SecuritySep 8, 20152 citations

Simple and flexible universal composability : definition of a framework and applications

Daniel Rausch

Security protocols, such as TLS, SSH, IEEE~802.11, and DNSSEC, have become crucial tools in modern society to protect people, data, and infrastructure. They are used throughout virtually all electronic devices to achieve a wide range of different security goals, such as confidentiality, authentication, and integrity. As the long history of attacks on security protocols illustrates, it is indispensable to perform a formal security analysis of such protocols. A central tool in cryptography for taming the complexity of the design and the analysis of modern protocols is modularity, provided by security models for universal composability. Such models allow for designing and analyzing small parts of a protocol in isolation and then reusing these security results in the context of the overall protocol. This is not just easier than analyzing the whole protocol as a monolithic block but also reduces the overall effort required in building and analyzing multiple different protocols based on the same underlying components, such as cryptographic primitives. Ideally, a model for universal composability should support a protocol designer in easily creating full, precise, and detailed specifications as well as sound security proofs of various protocols for various types of adversarial models, instead of being an additional obstacle one has to overcome during a security analysis. In particular, such a model should be sound, flexible/expressive, and easy to use. Unfortunately, despite the wide spread use of models for universal composability, existing models and frameworks are still unsatisfying in these respects as none combines all of these requirements simultaneously. In this thesis we therefore develop a model for universal composability, called the iUC framework, which combines soundness, usability, and flexibility in a so far unmatched way, and hence constitutes a solid framework for designing and analyzing essentially any protocol and application in a modular, universally composable, and sound manner. We use our model in a case study to analyze multiple different key exchange protocols precisely as they are deployed in practice. This illustrates the combination of both flexibility and usability of our model. This case study is also an important independent contribution as this is the first faithful security analysis of these unmodified protocols in a universal composability setting.

Jan 1, 20200 citations

ILC: a calculus for composable, computational cryptography

Kevin Liao, Matthew A. Hammer, Andrew Miller

The universal composability (UC) framework is the established standard for analyzing cryptographic protocols in a modular way, such that security is preserved under concurrent composition with arbitrary other protocols. However, although UC is widely used for on-paper proofs, prior attempts at systemizing it have fallen short, either by using a symbolic model (thereby ruling out computational reduction proofs), or by limiting its expressiveness.

ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)Jun 7, 201919 citations

Diving Deep Into UC

Céline Chevalier, Éric Sageloli

Introduced by Canetti in 2001, Universal Composability (UC) is a widely adopted security model that enables the specification and proof of security for a broad range of protocols, offering strong security guarantees. At its core lies the universal composition theorem (UC theorem), which ensures that protocols proven secure within the framework remain secure even when deployed in real-world environments with multiple instances of them. In this work, we present two key contributions. First, we identify several problems with the UC framework, in particular the UC Theorem. They include counterexamples, limitations that make it unusable for important classes of protocols, and weaknesses in its proof. These problems reveal flaws in nearly all the fundamental concepts of UC. Second, we propose a revised formulation of the main concepts of UC to address these issues. Although the resulting modifications are nontrivial, our updated definitions are designed to remain as faithful as possible to the structure and intent of the original model.

IACR Communications in CryptologyMay 4, 20260 citations

GNUC: A New Universal Composability Framework.

Dennis Hofheinz, Victor Shoup

We put forward a framework for the modular design and analysis of multi-party protocols. Our framework is called “GNUC ” (with the recursive meaning “GNUC’s Not UC”), already alluding to the similarity to Canetti’s Universal Composability (UC) framework. In particular, like UC, we offer a universal composition theorem, as well as a theorem for composing protocols with joint state. We deviate from UC in several important aspects. Specifically, we have a rather different view than UC on the structuring of protocols, on the notion of polynomial-time protocols and attacks, and on corruptions. We will motivate our definitional choices by explaining why the definitions in the UC framework are problematic, and how we overcome these problems. Our goal is to offer a framework that is largely compatible with UC, such that previous results formulated in UC carry over to GNUC with minimal changes. We exemplify this by giving explicit formulations for several important protocol tasks, including authenticated and secure communication, as well as commitment and secure function evaluation. 1

Jan 1, 201117 citations

Universally Composable Security: A New Paradigm for Cryptographic Protocols.

Ran Canetti

We present a general framework for representing cryptographic protocols and analyzing their security. The framework allows specifying the security requirements of practically any cryptographic task in a unified and systematic way. Furthermore, in this framework the security of protocols is preserved under a general protocol composition operation, called universal composition. The proposed framework with its security-preserving composition operation allows for modular design and analysis of complex cryptographic protocols from relatively simple building blocks. Moreover, within this framework, protocols are guaranteed to maintain their security in any context, even in the presence of an unbounded number of arbitrary protocol instances that run concurrently in an adversarially controlled manner. This is a useful guarantee, that allows arguing about the security of cryptographic protocols in complex and unpredictable environments such as modern communication networks.

Jan 1, 200085 citations