Track papers across labs, topics, and trends.
Search papers, labs, and topics across Lattice.
This paper applies category theory to enhance the understanding of Canetti's Universal Composability (UC) framework for static systems, utilizing string diagrams to provide a rigorous yet intuitive graphical representation of the composition theorem. The authors demonstrate that their categorical approach not only generalizes the framework beyond interactive Turing machines to include quantum computation and domain-specific languages but also allows for the relaxation of certain restrictions without loss of expressiveness. Key findings include the identification and correction of technical oversights in the standard UC formulation, which could improve the robustness of secure composition in various computational contexts.
A categorical approach reveals that secure composition can be visualized and verified graphically, correcting overlooked details in traditional frameworks.
Category theory is a mathematical theory of composition, widely used in logic, computing, and physics. Here we apply it to give a theory of secure composition. In particular, we provide a categorical treatment of Canetti's Universal Composability (UC) framework for systems with a static number of parties and sessions, often termed UC for static systems, yielding four benefits. First, we present our results graphically yet retain rigor by applying a standard categorical technique known as string diagrams. In particular, our formulation of the composition theorem can be graphically verified with a short sequence of diagrams, while remaining translatable to equations and amenable to formal verification. Second, categories let us generalize so that our results extend beyond interactive Turing machines to other forms of computation, such as quantum computation or domain-specific languages. Third, categories help us drop some unnecessary restrictions of UC (e.g., our adversary can be a computational network rather than a single Turing machine); we prove equivalence between our variant and the usual UC, showing no expressiveness is lost. Finally, the categorical perspective leads us to identify and correct some minor technical oversights in the standard formulation of simple UC.