Proof-theoretic cryptography is an emerging paradigm that grounds cryptographic security in the metatheory of linear logic proof nets, specifically the cut-elimination theorem. To enable modular construction and analysis of complex protocols in this paradigm, a compositional security framework is essential. In this paper, we propose such a framework, inspired by the Universal Composability (UC) framework but tailored to the algebraic structure of Multiplicative Linear Logic (MLL). We define a proof-net protocol as an MLL proof net with designated input/output interfaces and a partial order on its cut nodes. Two composition operators are naturally given by the logic: tensor product (⊗) for parallel composition and cut-elimination connection (◦) for sequential composition. We define an ideal functionality as a cut-free proof net together with a specification of its input/output behavior. We adopt a simulation-based security definition where the environment is an arbitrary PPT interactive Turingmachine (not restricted to proof nets), while the protocol and the adversary are described as proof-net protocols. This allows us to inherit the full power of the UC environment while keeping the protocol analysis within the proof-net framework. We then prove two composition theorems: if two protocols securely realize their respective ideal functionalities, then both their tensor product and their cut-elimination connection securely realize the corresponding compositions of the ideal functionalities. Theproofs rely on the confluence and strong normalization of cut elimination in MLL, which simplifies the analysis compared to general UC proofs, while still handling arbitrary environments. Finally, we discuss the relationship between our framework and the UC framework, clarifying that our framework is a specialization that exploits the algebraic structure of proof nets but does not sacrifice environmental generality. We also discuss the limitations of the current framework (static corruption, synchronousbroadcast) and outline directions for future generalization.
Proof-theoretic cryptography is an emerging paradigm that grounds cryptographic security in the metatheory of linear logic proof nets, specifically the cut-elimination theorem. To enable modular construction and analysis of complex protocols in this paradigm, a compositional security framework is essential. In this paper, we propose such a framework, inspired by the Universal Composability (UC) framework but tailored to the algebraic structure of Multiplicative Linear Logic (MLL). We define a proof-net protocol as an MLL proof net with designated input/output interfaces and a partial order on its cut nodes. Two composition operators are naturally given by the logic: tensor product (⊗) for parallel composition and cut-elimination connection (◦) for sequential composition. We define an ideal functionality as a cut-free proof net together with a specification of its input/output behavior. We adopt a simulation-based security definition where the environment is an arbitrary PPT interactive Turingmachine (not restricted to proof nets), while the protocol and the adversary are described as proof-net protocols. This allows us to inherit the full power of the UC environment while keeping the protocol analysis within the proof-net framework. We then prove two composition theorems: if two protocols securely realize their respective ideal functionalities, then both their tensor product and their cut-elimination connection securely realize the corresponding compositions of the ideal functionalities. Theproofs rely on the confluence and strong normalization of cut elimination in MLL, which simplifies the analysis compared to general UC proofs, while still handling arbitrary environments. Finally, we discuss the relationship between our framework and the UC framework, clarifying that our framework is a specialization that exploits the algebraic structure of proof nets but does not sacrifice environmental generality. We also discuss the limitations of the current framework (static corruption, synchronousbroadcast) and outline directions for future generalization.
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.
Fair multi-party computation (MPC) requires that either all parties learn the output or none do. Existing fair protocols either rely on a trusted third party, impose high round complexity, or lack post-quantum security. We propose a new fairness mechanism based on cut elimination in multiplicative linear logic (MLL) proof nets. Our key insight is that proof nets naturally encode partial orders among input revelations, enabling efficient handling of arbitrary dependencies while guaranteeing atomic release. We combine proof nets with post-quantum lattice-based equivocal commitments in the common reference string (CRS) model toachieve privacy. A malicious party who aborts before eliminating its cut node leaves the final cut locked; honest parties detect the abort and output nothing. We provide a rigorous security analysis that includes a formal real/ideal simulation-based definition of fairness and privacy, explicit simulator constructions, and a hybrid argument for indistinguishability. The privacy proof works for any function representable as a Boolean circuit: the simulator, given the output and the corrupted parties’ inputs, can compute a consistent input for each honest party via reverse propagation (back-propagation) on the circuit. This yields a polynomial-time simulator without any additional assumptions. We present a full Python implementation of the three-party conditional computation y = (x1 ∧x2)∨x3, demonstrating explicit proof-net construction, real cut elimination, andfairness enforcement. The scheme requires no trusted third party, has O(k) rounds where k ≤ n is the number of actually eliminated cuts, and is post-quantum secure when instantiated with lattice-based commitments
We propose a modification to the framework of Universally Composable (UC) security [3]. Our new notion involves comparing the real protocol execution with an ideal execution involving ideal functionalities (just as in UC-security), but allowing the environment and adversary access to some super-polynomial computational power. We argue the meaningfulness of the new notion, which in particular subsumes many of the traditional notions of security. We generalize the Universal Composition theorem of [3] to the new setting. Then under new computational assumptions, we realize secure multi-party computation (for static adversaries) without a common reference string or any other set-up assumptions, in the new framework. This is known to be impossible under the UC framework.
We propose a modification to the framework of Universally Composable (UC) security [3]. Our new notion, involves comparing the protocol executions with an ideal execution involving ideal functionalities (just as in UC-security), but allowing the environment and adversary access to some super-polynomial computational power. We argue the meaningfulness of the new notion, which in particular subsumes many of the traditional notions of security. We generalize the Universal Composition theorem of [3] to the new setting. Then under new computational assumptions, we realize secure multi-party computation (for static adversaries) without a common reference string or any other set-up assumptions, in the new framework. This is known to be impossible under the UC framework. 1
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.
Nowadays it is widely accepted to formulate the security of a protocol carrying out a given task via the “trustedparty paradigm,” where the protocol execution is compared with an ideal process where the outputs are computed by a trusted party that sees all the inputs. A protocol is said to securely carry out a given task if running the protocol with a realistic adversary amounts to “emulating” the ideal process with the appropriate trusted party. In the Universal Composability (UC) framework the program run by the trusted party is called an ideal functionality. While this simulation-based security formulation provides strong security guarantees, its usefulness is contingent on the properties and correct specification of the ideal functionality, which, as demonstrated in recent years by the coexistence of complex, multiple functionalities for the same task as well as by their “unstable” nature, does not seem to be an easy task. In this paper we address this problem, by introducing a general methodology for the sound specification of ideal functionalities. First, we introduce the class of canonical ideal functionalities for a cryptographic task, which unifies the syntactic specification of a large class of cryptographic tasks under the same basic template functionality. Furthermore, this representation enables the isolation of the individual properties of a cryptographic task as separate members of the corresponding class. By endowing the class of canonical functionalities with an algebraic structure we are able to combine basic functionalities to a single final canonical functionality for a given task. Effectively, this puts forth a bottom-up approach for the specification of ideal functionalities: first one defines a set of basic constituent functionalities for the task at hand, and then combines them into a single ideal functionality taking advantage of the algebraic structure. In our framework, the constituent functionalities of a task can be derived either directly or, following a translation strategy we introduce, from existing game-based definitions; such definitions have in many cases captured desired individual properties of cryptographic tasks, albeit in less adversarial settings. Our translation methodology entails a sequence of steps that systematically derive a corresponding canonical functionality given a game-based definition, effectively “lifting” the game-based definition to its composition-safe version. We showcase our methodology by applying it to a variety of basic cryptographic tasks, including commitments, digital signatures, zero-knowledge proofs, and oblivious transfer. While in some cases our derived canonical functionalities are equivalent to existing formulations, thus attesting to the validity of our approach, in others they differ, enabling us to “debug” previous definitions and pinpoint their shortcomings.