We formalize the simulation paradigm of cryptography in terms of category theory and show that protocols secure against abstract attacks form a symmetric monoidal category, thus giving an abstract model of composable security definitions in cryptography. Our model is able to incorporate computational security, set-up assumptions and various attack models such as colluding or independently acting subsets of adversaries in a modular, flexible fashion. We conclude by using string diagrams to rederive no-go results concerning the limits of bipartite and tripartite cryptography, ruling out composable commitments and broadcasting.
On the way, we exhibit two categorical constructions of resource theories that might be of independent interest: one capturing resources shared among $n$ parties and one capturing resource conversions that succeed asymptotically.

§ INTRODUCTION

Modern cryptographic protocols are complicated algorithmic entities, and their security analyses are often no simpler than the protocols themselves. Given this complexity, it would be highly desirable to be able to design protocols and reason about them compositionally, by breaking them down into smaller constituent parts. In particular, one would hope that combining protocols proven secure results in a secure protocol without need for further security proofs. However, this is not the case for stand-alone security notions that are common in cryptography. To illustrate such failures of composability, let us consider the history of quantum key distribution (QKD), as recounted in <cit.>: QKD was originally proposed in 80s <cit.>. The first security proofs against unbounded adversaries followed a decade later <cit.>. However, since composability was originally not a concern, it was later realized that the original security definitions did not provide a good enough level of security <cit.>—they didn't guarantee security if the keys were to be actually used, since even a partial leak of the key would compromise the rest. The story ends on a positive note, as eventually a new security criterion was proposed, together with stronger proofs <cit.>.

In this work we initiate a categorical study of composable security definitions in cryptography. In the viewpoint developed here one thinks of cryptography as a resource theory: cryptographic functionalities (e.g. secure communication channels) are viewed as resources and cryptographic protocols let one transform some starting resources to others. For instance, one can view the one-time-pad as a protocol that transforms an authenticated channel and a shared secret key into a secure channel. For a given protocol, one can then study whether it is secure against some (set of) attack model(s), and protocols secure against a fixed set of models can always be composed sequentially and in parallel.

This is in fact the viewpoint taken in constructive cryptography <cit.>, which also develops the one-time-pad example above in more detail. However <cit.> does not make a formal connection to resource theories as usually understood, whether as in quantum physics <cit.>, or more generally as defined in order theoretic <cit.> or categorical <cit.> terms. Instead, constructive cryptography is usually combined with abstract cryptography <cit.> which is formalized in terms of a novel algebraic theory of systems <cit.>.

Our work can be seen as a particular formalization of the ideas behind constructive cryptography, or alternatively as giving a categorical account of the real-world-ideal-world paradigm (also known as the simulation paradigm <cit.>), which underlies more concrete frameworks for composable security, such as universally composable cryptography <cit.> and others <cit.>.  We will discuss these approaches and  abstract and constructive cryptography in more detail in Section <ref>

Our long-term goal is to enable cryptographers to reason about composable security at the same level of formality as stand-alone security, without having to fix all the details of a machine model nor having to master category theory. Indeed, our current results already let one define multipartite protocols and security against arbitrary subsets of malicious adversaries in any symmetric monoidal category $\C$. Thus, as long as one's model of interactive computation results in a symmetric monoidal category, or more informally, one is willing to use pictures such as <ref> to depict connections between computational processes without further specifying the order in which the picture was drawn, one can use the simulation paradigm to reason about multipartite security against malicious participants composably—and specifying finer details of the computational model is only needed to the extent that it affects the validity of one's argument. Moreover, as our attack models and composition theorems are fairly general, we hope that more refined models of adversaries can be incorporated.

We now highlight our contributions to cryptography:

* We show how to adapt resource theories as categorically formulated <cit.> in order to reason abstractly about secure transformations between resources. This is done in Section <ref> by formalizing the simulation paradigm in terms of an abstract attack model (Definition <ref>), designed to be general enough to capture standard attack models of interest (and more) while still structured enough to guarantee composability. This section culminates in Corollary <ref>, which shows that for any fixed set of attack models, the class of protocols secure against each of them results in a symmetric monoidal category. In Theorem <ref> we observe that under suitable conditions, images of secure protocols under monoidal functors remain secure, which gives an abstract variant of the lifting theorem <cit.> that states that perfectly UC-secure classical protocols are also quantum UC-secure.

* We adapt this framework to model computational security in <ref> in two ways: either by replacing equations with an equivalence relation, abstracting the idea of computational indistinguishability, or by working with a notion of distance. In the case of a distance, one can then either explicitly bound the distance between desired and actually achieved behavior, or work with sequences of protocols that converge to the target in the limit: the former models working in the finite-key regimen <cit.>  and the latter models the kinds of asymptotic security and complexity statements that are common in cryptography. In the former case we show that errors compose additively in Lemma <ref>, and in Theorem <ref> and in Corollary <ref> we show that protocols that are correct in the limit can be composed at will.

* Finally, we apply the framework developed to study bipartite and tripartite cryptography. We  reprove the no-go-theorems of <cit.> concerning two-party commitments (and three-party broadcasting) in this setting, and reinterpret them as limits on what can be achieved securely in any compact closed category (symmetric monoidal category). The key steps of the proof are done graphically, thus opening the door for cryptographers to use such pictorial representations as rigorous tools rather than merely as illustrations.

Moreover, we discuss some categorical constructions on resource theories capturing aspects of resource theories appearing in the physics literature. These contributions may be  relevant for further categorical studies on resource theories, independently of their usage here.

* In <cit.> it is observed that many resource theories arise from an inclusion $\cat{C}_F\hookrightarrow\cat{C}$ of free transformations into a larger monoidal category, by taking the resource theory of states. We observe that this amounts to applying the monoidal Grothendieck construction <cit.> to the functor $\CF\to\C\xrightarrow{\hom(I,-)}\cat{Set}$. This suggests applying this construction more generally to the composite of monoidal functors $F\colon\cat{D}\to\cat{C}$ and  $R\colon \cat{C}\to\Set$.

* In Example <ref> we note that choosing $F$ to be the $n$-fold monoidal product $\C^n\to\C$ captures resources shared by $n$ parties and $n$-partite transformations between them.

* In <ref> we model categorically situations where there is a notion of distance between resources, and instead of exact resource conversions one either studies approximate transformations or sequences of transformations that succeed in the limit.

* In <ref> we discuss a variant of a construction on monoidal categories, used in special cases in <cit.> and discussed in more detail in <cit.>, that allows one to declare some resources free and thus enlarge the set of possible resource conversions.

§.§ Related work

We have already mentioned that cryptographers have developed a plethora of frameworks for composable security, such as universally composable cryptography <cit.>, reactive simulatability <cit.> and others <cit.>. Moreover, some of these frameworks have been adapted to the quantum setting <cit.>. One might hence be tempted to think that the problem of composability in cryptography has been solved. However, it is fair to say that most mainstream cryptography is not formulated composably and that composable cryptography has yet to realize its full potential. Moreover, this proliferation of frameworks should be taken as evidence of the continued importance of the issue, and is in fact reflected by the existence of a recent Dagstuhl seminar on this matter <cit.>. Indeed, the aforementioned frameworks mostly consist of setting up fairly detailed models of interacting machines, which as an approach suffers from two drawbacks:

* In order to be more realistic, the detailed models are often complicated to reason in terms of and even to define, thus making practicing cryptographers less willing to use them. Perhaps more importantly it is not always clear whether the results proven in a particular model apply more generally for other kinds of machines, whether those of a competing framework or those in the real world. It is true that the choice of a concrete machine model does affect what can be securely achieved—for instance, quantum cryptography differs from classical cryptography and similarly classical cryptography behaves differently in synchronous and asynchronous settings <cit.>. Nevertheless, one might hope that composable cryptography could be done at a similar level of formality as complexity theory, where one rarely worries about the number of tapes in a Turing machine or of other low-level details of machine models.

* Changing the model slightly (to model different kinds of adversaries or to incorporate a different notion of efficiency) often requires reproving “composition theorems” of the framework or at least checking that the existing proof is not broken by the modification.

In contrast to frameworks based on detailed machine models, there are two closely related top-down approaches to cryptography: constructive cryptography <cit.> and its cousin abstract cryptography <cit.>. We are indebted to both of these approaches, and indeed our framework could be seen as formalizing the key idea of constructive cryptography—namely, cryptography as a resource theory—and thus occupying a similar space as abstract cryptography. A key difference is that constructive cryptography is usually instantiated in terms of abstract cryptography <cit.>, which in turn is based on a novel algebraic theory of systems <cit.>. However, our work is not merely a translation from this theory to categorical language, as there are important differences and benefits that stem from formalizing cryptography in terms of an well-established and well-studied algebraic theory of systems—that of (symmetric) monoidal categories:

* The fact that cryptographers wish to compose their protocols sequentially and in parallel strongly suggests using monoidal categories, that have these composition operations as primitives. In our framework, protocols secure against a fixed set of attack models results in a symmetric monoidal category. In contrast, the algebraic theory of systems <cit.> on which abstract cryptography is based  takes parallel composition and internal wiring as its primitives. This design choice results in some technical kinks and tangles that are natural with any novel theory but have already been smoothed out in the case of category theory. For instance, in the algebraic theory of systems of <cit.> the parallel composition is a partial operation and in particular the parallel composite of a system with itself is never defined[While the suggested fix is to assume that one has “copies” of the same system with disjoint wire labels, it is unclear how one recognizes or even defines in terms of the system algebra that two distinct systems are copies of each other.] and the set of wires coming out of a system is fixed once and for all[Indeed, while <cit.> manages to bundle and unbundle ports along isomorphism when convenient, it seems like the chosen technical foundation makes this more of a struggle than it should be.]. In contrast, in a monoidal category parallel composition is a total operation and whether one draws a box with $n$ output wires of types $A_1,\dots A_n$ or single output wire of type $\bigotimes_{i=1}^n A_i$ is a matter of convenience. Technical differences such as these make a direct formal comparison or translation between the frameworks difficult, even if informally and superficially there are similarities.

* We do not abstract away from an attacker model, but rather make it an explicit part of the formalism that can be modified without worrying about composability. This makes it possible to consider and combine very easily different security properties, and in particular paves the way to model attackers with limited powers such as honest-but-curious adversaries. In our framework, one can first fix a protocol transforming some resource to another one, and then discuss whether this transformation is secure against different attack models. In contrast, in abstract cryptography a cryptographic resource is a tuple of functionalities, one for each set of dishonest parties, and thus has no prior existence before fixing the attack model. This makes the question “what attack models is this protocol secure against?” difficult to formalize.

* As category theory is de facto the lingua franca between several subfields of mathematics and computer science, elucidating the categorical structures present in cryptography opens up the door to further connections between cryptography and other fields. For instance, game semantics readily gives models of interactive, asynchronous and probabilistic (or quantum) computation <cit.> in which our theory can be instantiated, and thus further paves the way for programming language theory to inform cryptographic models of concurrency.

* Category theory comes with existing theory, results and tools that can readily be applied to questions of cryptographic interest. In particular the graphical calculi of symmetric monoidal and compact closed categories <cit.> enables one to rederive impossibility results shown in <cit.> purely pictorially. In fact, such pictures were already often used as heuristic devices that illuminate the official proofs, and viewing these pictures categorically lets us promote them from mere illustrations to rigorous yet intuitive proofs. Indeed, in <cit.> the authors suggest moving from a 1-dimensional symbolic presentation to a 2-dimensional one, and this is exactly what the graphical calculus already achieves.

The approaches above result in a framework where security is defined so as to guarantee composability. In contrast, approaches based on various protocol logics <cit.> aim to characterize situations where composition can be done securely, even if one does not use composable security definitions throughout. As these approaches are based on process calculi, they are categorical under the hood <cit.> even if not overtly so. There is also earlier work explicitly discussing category theory in the context of cryptography <cit.>, but they concern stand-alone security of particular (kinds of) cryptographic protocols, rather than categorical aspects of composable security definitions.

§ RESOURCE THEORIES

We briefly review the categorical viewpoint on resource theories of <cit.>. Roughly speaking, a resource theory can be seen as a SMC but the change in terminology corresponds to a change in viewpoint: usually in category theory one studies global properties of a category, such as the existence of (co)limits, relationships to other categories, etc. In contrast, when one views a particular SMC $\C$ as resource theory, one is interested in local questions. One thinks of objects of $\C$ as resources, and morphisms as processes that transform a resource to another. From this point of view, one mostly wishes to understand whether $\hom_\C(X,Y)$ is empty or not for resources $X$ and $Y$ of interest. Thus from the resource-theoretic point of view, most of the interesting information in $\C$ is already present in its preorder collapse. As concrete examples of resource-theoretic questions, one might wonder if

* some noisy channels can simulate a (almost) noiseless channel <cit.>

* there is a protocol that uses only local quantum operations and classical communication and transforms a particular quantum state to another one <cit.>

* some non-classical statistical behavior can be used to simulate other such behavior <cit.>

In <cit.> the authors show how many familiar resource theories arise in a uniform fashion: starting from an SMC $\C$ of processes equipped with a wide sub-SMC $\CF$ whose morphisms correspond to “free” processes, they build several resource theories (=SMCs). Perhaps the most important of these constructions is the resource theory of states: given $\CF\hookrightarrow\C$, the corresponding resource theory of states can be explicitly constructed by taking the objects of this resource theory to be states of $\C$, maps $r\colon I\to A$ for some $A$, and maps $r\to s$ are maps $f\colon A\to B$ in $\CF$ that transform $r$ to $s$ as in <ref>.

We now turn our attention towards cryptography. As contemporary cryptography is both broad and complex in scope, any faithful model of it is likely to be complicated as well. A benefit of the categorical idiom is that we can build up to more complicated models in stages, which is what we will do in the sequel. We phrase our constructions in terms of an arbitrary SMC $\C$, but in order to model actual cryptographic protocols, the morphisms of $\C$ should represent interactive computational machines with open “ports”, with composition then amounting to connecting such machines together. Different choices of $\C$ set the background for different kinds of cryptography, so that quantum cryptographers want $\C$ to include quantum systems whereas in classical cryptography it is sufficient that these computational machines are probabilistic. Constructing such categories $\C$ in detail is not trivial but is outside our scope—we will discuss this in more detail in section <ref>.

Our first observation is that there is no reason to restrict to inclusions $\CF\hookrightarrow\C$ in order to construct a resource theory of states. Indeed, while it is straightforward to verify explicitly that the resource theory of states is a symmetric monoidal category, it is instructive to understand more abstractly why this is so: in effect, the constructed category is the category of elements of the composite functor $\CF\to\C\xrightarrow{\hom(I,-)}\cat{Set}$. As this composite is a (lax) symmetric monoidal functor, the resulting category is automatically symmetric monoidal as observed in <cit.>. Thus this construction goes through for any symmetric (lax) monoidal functors $\cat{D}\xrightarrow{F}\cat{C}\xrightarrow{R}\Set$. Here we may think of $F$ as interpreting free processes into an ambient category of all processes, and $R\colon\C\to\cat{Set}$ as an operation that gives for each object $A$ of $\C$ the set $R(A)$ of resources of type $A$.

Explicitly, given symmetric monoidal functors $\cat{D}\xrightarrow{F}\cat{C}\xrightarrow{R}\Set$, the category of elements $\res RF$ has as its objects pairs $(r,A)$ where $A$ is an object of $\cat{D}$ and $r\in RF(A)$, the intuition being that $r$ is a resource of type $F(A)$. A morphism $(r,A)\to (s,B)$ is given by a morphism $f\colon A\to B$ in $\cat{D}$ that takes $r$ to $s$, satisfies $RF(f)(r)=s$. The symmetric monoidal structure comes from the symmetric monoidal structures of $\cat{D}, \Set$ and $RF$. Somewhat more explicitly, $(r,A)\otimes (s,B)$ is defined by $(r\otimes s,A\otimes B)$ where $r\otimes s$ is the image of $(r,s)$ under the function $RF(A)\times RF(B)\to RF(A\otimes B)$ that is part of the monoidal structure on $RF$, and on morphisms of $\res RF$ the monoidal product is defined from that of $\cat{D}$.

From now on we will assume that $F$ is strong monoidal, and while $R=\hom(I,-)$ captures our main examples of interest, we will phrase our results for an arbitrary lax monoidal $R$. This relaxation allows us to capture the $n$-partite structure often used when studying cryptography, as shown next.

Consider the resource theory induced by $\C^n\xrightarrow{\otimes}\C\xrightarrow{\hom(I,-)}\Set$, where we write $\otimes$ for the $n$-fold monoidal product[As $\C$ is symmetric, the functor $\otimes$ is strong monoidal.]. The resulting resource theory has a natural interpretation in terms of $n$ agents trying to transform resources to others: an object of this resource theory corresponds to a pair $((A_i)_{i=1}^n,r\colon I\to \bigotimes A_i)$, and can be thought of as an $n$-partite state, depicted in <ref>, where the $i$-th agent has access to a port of type $A_i$.
A morphism $\f=(f_1,\dots f_n)\colon ((A_i)_{i=1}^n,r)\to ((B_i)^n_{i=1},s)$ between such resources then amounts to a protocol that prescribes, for each agent $i$ a process $f_i$ that they should perform so that $r$ gets transformed to $s$ as in <ref>.

\[\begin{pic}
\node[morphism] (f) at (0,.5) {$f$};
\node[state] (x) at (0,0) {$r$};
\draw (f.south) to node[right] {$$} (x.north);
\draw (f.north) to +(0,.3) node[right] {};
\end{pic}=\begin{pic}
\node[state] (y) at (0,0) {$s$};
\draw (y.north) to +(0,1);
\end{pic}\]
\caption{A map in the resource theory of states}
\label{fig:state_transform}
\end{subfigure}
\begin{subfigure}[b]{0.23\textwidth}
\[
\begin{pic}
\node[state] (f) at (0,0) {$s$};
\node (a) at (0,.25) {$\ldots$};
\draw ([xshift=-1.5pt]f.A) to +(0,.5) node[left] {$A_1$};
\draw ([xshift=1.5pt]f.B) to +(0,.5) node[right] {$A_n$};
\end{pic}
\]
\caption{An $n$-partite state}
\label{fig:n-partite_state}
\end{subfigure}
\begin{subfigure}[b]{0.23\textwidth}
\[
\begin{pic}
\node[state] (r) at (0,0) {$r$};
\node (a) at (0,.25) {$\ldots$};
\node[morphism,scale=.5,font=\normalsize] (f) at (-.28,.5) {$f_1$};
\node[morphism,scale=.5,font=\normalsize] (g) at (.28,.5) {$f_n$};
\draw ([xshift=-1.5pt]r.A) to (f.south);
\draw ([xshift=1.5pt]r.B) to (g.south);
\draw (f.north) to +(0,.3);
\draw (g.north) to +(0,.3);
\end{pic}\quad=
\begin{pic}
\node[state] (f) at (0,0) {$s$};
\node (a) at (0,.25) {$\ldots$};
\draw ([xshift=-1.5pt]f.A) to +(0,.5) node[left] {$B_1$};
\draw ([xshift=1.5pt]f.B) to +(0,.5) node[right] {$B_n$};
\end{pic}
\]
\caption{An $n$-partite transformation}
\label{fig:n-partite_state_transformation}
\end{subfigure}
\[\begin{pic}
\node[morphism] (g) at (0,0) {$g'$};
\node[morphism] (f) at (1,0) {$f'$};
\setlength\minimummorphismwidth{13mm}
\node[morphism] (h) at (0.5,1) {$h'$};
\draw (g.north) to ([xshift=0.5pt]h.south west);
\draw (f.north) to ([xshift=-0.5pt]h.south east);
\draw (h.north) to +(0,.3);
\draw (g.south) to +(0,.-.3);
\draw (f.south) to +(0,.-.3);
\end{pic}
\]
\caption{Factorization of an attack on $f\otimes g$}
\label{fig:attackonprod}
\end{subfigure}
\end{figure}
\end{example}
In this resource theory, all of the agents are equally powerful and can perform all processes allowed by $\C$, and this might be unrealistic: first of all, $\C$ might include computational processes that are too powerful/expensive for us to use in our cryptographic protocols. Moreover, having agents with different computational powers is important to model \eg blind quantum computing~\cite{BFK09} where a client with access only to limited, if any, quantum computation tries to securely delegate computations to a server with a powerful quantum computer. This limitation is easily remedied: we could take the $i$-th agent to be able to implement computations in some sub-SMC $\C_i$ of $\C$, and then consider $\prod_{i=1}^n \C_i\to\C$.

A more serious limitation is that such transformations have no security guarantees---they only work if each agent performs~$f_i$ as prescribed by the protocol. We fix this next.

\section{Cryptography as a resource theory}\label{sec:crypto}
\begin{figure}
\centering
\begin{subfigure}[b]{0.3\textwidth}
\[\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[state] (r) at (0,0) {$r$};
\node (a) at (-.23,.2) {$\ldots$};
\node[morphism,scale=.5,font=\normalsize] (f) at (-.5,.5) {$f_1$};
\node[morphism,scale=.5,font=\normalsize] (h) at (0,.5) {$f_{k}$};
\node[morphism,scale=.5,font=\normalsize] (g) at (.5,.5) {$a$};
\draw ([xshift=-3.5pt]r.A) to (f.south);
\draw ([xshift=3.5pt]r.B) to (g.south);
\draw (f.north) to +(0,.3);
\draw (g.north) to +(0,.3);
\draw (h.north) to +(0,.3);
\draw (r.center) to (h.south);
\end{pic}\text{ or }
\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (f) at (-.28,.5) {$\f|_{[k]}$};
\node[morphism,scale=.5,font=\normalsize] (g) at (.28,.5) {$a$};
\node[state,scale=1.25] (x) at (0,0) {$r$};
\draw (f.south) to node[left] {$[k]$} (x.A);
\draw (f.north) to +(0,.3) node[right] {};
\draw (g.south) to node[right] {$[n]\setminus [k]$} (x.B);
\draw (g.north) to +(0,.3) node[right] {};
\end{pic}\]
\caption{Attack by the $n$-th party}
\label{fig:attack}
\end{subfigure}
\begin{subfigure}[b]{0.3\textwidth}
\[\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (f) at (-.28,.5) {$f|_{[k]}$};
\node[morphism,scale=.5,font=\normalsize] (g) at (.28,.5) {$a$};
\node[state,scale=1.25] (x) at (0,0) {$r$};
\draw (f.south) to node[left] {$[k]$} (x.A);
\draw (f.north) to +(0,.3) node[right] {};
\draw (g.south) to node[right] {$[n]\setminus [k]$} (x.B);
\draw (g.north) to +(0,.3) node[right] {};
\end{pic}=\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (g) at (.28,.5) {$b$};
\node[state,scale=1.25] (x) at (0,0) {$s$};
\draw (x.A) to node[left] {$[k]$} +(0,.35) to +(0,.95);
\draw (g.south) to node[right] {$[n]\setminus [k]$} (x.B);
\draw (g.north) to +(0,.3) node[right] {};
\end{pic}.\]
\caption{Security against the parties $k+1,\dots n$}
\label{fig:security}
\end{subfigure}
\begin{subfigure}[b]{0.3\textwidth}
\[\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (f) at (-.28,.5) {$f|_{[k]}$};
\node[state,scale=1.25] (x) at (0,0) {$r$};
\draw (f.south) to node[left] {$[k]$} (x.A);
\draw (f.north) to +(0,.3) node[right] {};
\draw (x.B) to node[right]  {$[n]\setminus [k]$} +(0,.35)  to +(0,.95);
\end{pic}=\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (g) at (.28,.5) {$b$};
\node[state,scale=1.25] (x) at (0,0) {$s$};
\draw (x.A) to node[left] {$[k]$} +(0,.35) to +(0,.95);
\draw (g.south) to node[right] {$[n]\setminus [k]$} (x.B);
\draw (g.north) to +(0,.3) node[right] {};
\end{pic}\]
\caption{Security against the initial attack}
\label{fig:initial_attack}
\end{subfigure}
\end{figure}
In order for a protocol  $\f=(f_1,\dots ,f_n)\colon ((A_i)_{i=1}^n,r)\to ((B_i)^n_{i=1},s)$ to be secure, we should have some guarantees what happens if, as a result of \emph{an attack} on the protocol, something else than $(f_1,\dots ,f_n)$ happens. For instance, some subset of the parties might deviate from the protocol and do something else instead. In the simulation paradigm, security is then defined by saying that, anything that could happen when running the real protocol, \ie,  $\f$ with $r$, could also happen in the ideal world, \ie with $s$. A given protocol might be secure against some kinds of attacks and insecure against others, so we define security against an abstract attack model. This abstract notion of an attack model is one of the main definitions of our paper. It isolates conditions needed for the composition theorem~\ref{thm:composition}. It also captures our key examples that we use to illustrate the definition after giving it. Note that proofs that aren't immediate can be found in~\cref{sec:proofs}.
\begin{definition}\label{def:attack} An \emph{attack model} $\A$ on  an SMC $\C$ consists of giving for each morphism $f$ of $\C$ a class $\A(f)$ of morphisms of $\C$ such that
\begin{enumerate}[(i)]
\item $f\in\A(f)$ for every $f$.
\item For any $f\colon A\to B$ and $g\colon B\to C$ and composable $g'\in \A(g),f'\in \A(f)$ we have $g'\circ f'\in \A(g\circ f)$.
Moreover, any $h\in \A(g\circ f)$ factorizes as $g'\circ f'$ with $g'\in \A(g)$ and $f'\in \A(f)$.
\item For any $f\colon A\to B$, $g\colon C\to D$ in $\cat{C}$ and $f'\in \A(f), g'\in \A(g)$ we have $f'\otimes g'\in \A(f\otimes g)$. Moreover, any $h\in \A(f\otimes g)$ factorizes as $h'\circ (f'\otimes g')$ with $f'\in \A(f)$, $g'\in \A(g)$ and $h'\in \A(\id[B\otimes D])$.
\end{enumerate}
Let $f\colon (A,r)\to (B,s)$ define a morphism in the resource theory $\res RF$ induced by $F\colon\cat{D}\to\cat{C}$ and $R\colon \cat{C}\to\cat{Set}$. We say that $f$ is \emph{secure} against an attack model $\A$ on $\cat{C}$ (or $\A$-secure) if for any $f'\in \A(F(f))$ with $\dom(f')=F(A)$ there is $b\in\A(\id[F(B)])$ such that $R(f')r=R(b)s$.
\end{definition}
In the definition above we are asking for perfect equality which usually is too stringent a requirement for the purposes of cryptography. We will relax this requirement in Section~\ref{sec:computationalsecurity}.

The intuition is that $\A$ gives, for each process in $\C$, the set of behaviors that the attackers could force to happen instead of honest behavior. Then property (i) amounts to the assumption that the adversaries could behave honestly. The first halves of properties (ii) and (iii) say that, given an attack on $g$ and one on $f$, both attacks could happen when composing $g$ and~$f$ sequentially or in parallel. The second parts of these say that attacks on composite processes can be understood as composites of attacks. However, note that (iii) does not say that an attack on a product has to be a product of attacks: the factorization says that any $h\in\A(g\otimes f)$ factorizes as in \cref{fig:attackonprod} with $g'\in \A(g)$, $f'\in \A(f)$ and $h'\in \A(\id[B\otimes D])$. The intuition is that an attacker does not have to attack two parallel protocols independently of each other, but might play the protocols against each other in complicated ways. This intuition also explains why we do not require that all morphisms in $\A(f)$ have $F(A)$ as their domain, despite the  definition of $\A$-security quantifying only against those: when factoring $h\in \A(g\circ f)$  as $g'\circ f'$ with  $g'\in \A(g)$ and $f'\in \A(f)$, we can no longer guarantee that $F(B)$ is the domain of $g'$---perhaps the attackers take us elsewhere when they perform~$f'$.

If one thinks of $F\colon\cat{D}\to\cat{C}$ as representing the inclusion of free processes into general processes, one also gets an explanation why we do not insist that free processes and attacks live in the same category, \ie that $F=\id[\C]$. This is simply because we might wish to prove that some protocols are secure against attackers that can use more resources than we wish or can use in the protocols.
\begin{example} For any SMC $\C$ there are two trivial attack models: the minimal one defined by $\A(f)=\{f\}$ and the maximal one sending $f$ to the class of all morphisms of $\C$. We interpret the minimal attack model as representing honest behavior, and the maximal one as representing arbitrary malicious behavior.
\end{example}
\begin{proposition} If $\A_1,\dots ,\A_n$ are attack models on SMCs $\C_1,\dots ,\C_n$ respectively, then there is a product $\prod_{i=1}^n\A_i$ attack model on $\prod_{i=1}^n\C_i$ defined by $(\prod_{i=1}^n \A_i)(f_1,\dots, f_n)=\prod_{i=1}^n \A_i(f_i)$.
\end{proposition}
This proposition, together with the minimal and maximal attack models, is already expressive enough to model  multi-party computation where some subset of the parties might do arbitrary malicious behavior. Indeed, consider the $n$-partite resource theory induced by $\C^n\xrightarrow{\otimes}\C\xrightarrow{\hom(I,-)}\Set$. Let us first model a situation where the first $n-1$ participants are honest and the last participant is dishonest.  In this case we can set $\A=\prod_{i=1}^n \A_i$ where each of $\A_1,\dots ,\A_{n-1}$ is the minimal attack model on $\C$ and $\A_n$ is the maximal attack model.  Then, an attack on $\f=(f_1,\dots f_n)\colon ((A_i)_{i=1}^n,r)\to ((B_i)^n_{i=1},s)$ can be represented by the first $n-1$ parties obeying the protocol and the $n$-th party doing an arbitrary computation~$a$, as depicted in  the two pictures of \cref{fig:attack},
where $k=n-1$ and $\f|_{[k]}:=\bigotimes_{i=1}^k f_i$. The latter representation will be used when we do not need to emphasize pictorially the fact that the honest parties are each performing their own individual computations.

If instead of just one attacker, there are several \emph{independently} acting adversaries, we can take $\A=\prod_{i=1}^n \A_i$ where $\A_i$ is the minimal or maximal attack structure depending on whether the $i$-th participant is honest or not. If the set of dishonest parties can collude and communicate arbitrarily during the process, we need the flexibility given in Definition~\ref{def:attack} and have the attack structure live in a different category than where our protocols live. For simplicity of notation, assume that the first~$k$ agents are honest but the remaining parties are malicious and might do arbitrary (joint) processes in $\C$. In particular, the action done by the dishonest parties $k+1,\dots , n$ need not be describable as a product $\bigotimes_{i=k+1}^n (a_i)$ of individual actions.  In that case we define $\A$ as follows: we first consider our resource theory as arising from $\C^n\xrightarrow{\id^k\times\otimes}\C^k\times C\xrightarrow{\otimes}\C\xrightarrow{\hom(I,-)}\Set$, and define $\A$ on $\C^k\times \C$ as the product of the minimal attack model on $\C^k$ and the maximal one on $\C$. Concretely, this means that the first $k$ agents always obey the protocol, but the remaining agents can choose to perform arbitrary joint behaviors in $\C$. Then a generic attack on a protocol $\f$ can be represented exactly as before in \cref{fig:attack}, except we no longer insist that $k=n-1$. Now a protocol $\f$ is $\A$-secure if for any $a\in\A(\f)$ with $\dom(a)=(A_i)_{i=1}^n$ there is a $b\in\A(\id[B])$ satisfying the equation of \cref{fig:security}.

If one is willing to draw more wire crossings, one can easily depict and define security against an arbitrary subset of the parties behaving maliciously, and henceforward this is the attack model we have in mind when we say that some $n$-partite protocol is secure against some subset of the parties. Moreover, for any subset $J$ of dishonest agents, one could consider more limited kinds of attacks: for instance, the agents might have limited computational power or limited abilities to perform joint computations---as long as the attack model satisfies the conditions of Definition~\ref{def:attack} one automatically gets a composable notion of secure protocols by Theorem~\ref{thm:composition} below.
\begin{restatable}{theorem}{composition}\label{thm:composition} Given symmetric monoidal functors $F\colon\cat{D}\to\cat{C}$,  $R\colon \cat{C}\to\Set$ with $F$ strong monoidal and $R$ lax monoidal, and an attack model $\A$ on $\cat{C}$, the class of $\A$-secure maps forms a wide sub-SMC of the resource theory $\res RF$ induced by $RF$.
\end{restatable}
\noindent So far we have discussed security only against a single, fixed subset of dishonest parties, while in multi-party computation it is common to consider security against any subset containing \eg at most $n/3$ or $n/2$ of the parties. However, as monoidal subcategories are closed under intersection, we immediately obtain composability against multiple attack models.
\begin{corollary}\label{cor:simultaneoussafety}
Given a non-empty family of functors $(\cat{D}\xrightarrow{F_i}\cat{C_i}\xrightarrow{R_i}\Set)_{i\in I}$ with  $R_iF_i=R_jF_j=:R$ for all $i,j\in I$  and attack models $\A_i$ on $\C_i$ for each $i$, the class of maps in $\res R$ that is secure against each $\A_i$ is a sub-SMC of $\res R$.
\end{corollary}
Using Corollary~\ref{cor:simultaneoussafety} one readily obtains composability of protocols that are simultaneously secure against different attack models $\A_i$. Thus one could, in principle, consider composable cryptography in an $n$-party setting where some subsets are honest-but-curious, some might be outright malicious but have limited computational power, and some subsets might be outright malicious but not willing or able to coordinate with each other, without reproving any composition theorems.

While the security definition of $f$ quantifies over $\A(f)$, which may be infinite, under suitable conditions it is sufficient to check security only on a subset of $\A(f)$, so that whether $f$ is $\A$-secure often reduces to finitely many equations.

\begin{definition}\label{def:initialattack}
Given $f\colon A\to B$, a subset $X$  of $\A(f)$ is said to be \emph{initial} if any $f'\in\A(f)$ with $\dom(f')=A$ can be factorized as $b\circ a$ with $a\in X$ and $b\in\A(\id[B])$.
\end{definition}
\begin{theorem}
Let $f\colon (A,r)\to (B,s)$ define a morphism in the resource theory induced by $F\colon\cat{D}\to\cat{C}$ and $R\colon \cat{C}\to\cat{Set}$ and let $\A$ be an attack model on $\C$. If $X\subset\A(f)$ is initial, then $f$ is $\A$-secure if, and only if the security condition holds against attacks in $X$, \ie, if for any $f'\in X$ with $\dom(f')=F(A)$ there is $b\in\A(\id[F(B)])$ such that $R(f')r=R(b)s$.
\end{theorem}

Let us return to the example of $\C^n\to\C$ with the first $k$ agents being honest and the final $n-k$ dishonest and collaborating. Then we can take a singleton as our initial subset of attacks on $\f$, and this is given by $\f|_{[k]}\otimes (\bigotimes_{i=k+1}^n\id)$. Intuitively, this represents a situation where the dishonest parties $k+1,\dots ,n$ merely stand by and forward messages between the environment and the functionality without interfering, so that initiality can be seen as explaining ``completeness of the dummy adversary''~\cite[Claim 11]{Can01} in UC-security. In this case the security condition can be equivalently phrased by saying that there exists $b\in\A([\id[b]])$ satisfying the equation of \cref{fig:initial_attack},
which reproduces the pictures of~\cite{MT13}. Similarly, for  classical honest-but-curious adversaries one usually only considers the initial such adversary, who follows the protocol otherwise except that they keep track of the protocol transcript.
\begin{restatable}{theorem}{perfectlifting}\label{thm:perfectlifting}
In the resource theory of $n$-partite states, if $(f_1,\dots f_n)$ is secure  against some subset $J$ of $[n]$ and $F$ is a strong monoidal, then $(Ff_1,\dots, Fn)$ is secure against~$J$ as well.
\end{restatable}
\noindent For instance, if the inclusion of classical interactive computations into quantum ones is strong monoidal, \ie respects sequential and parallel composition (up to isomorphism), then unconditionally secure classical protocols are also secure in the quantum setting, as shown in the context of UC-security in~\cite[Theorem 15]{Unr10}. More generally, this result implies that the construction of the category of $n$-partite transformations secure against any fixed subset of $[n]$ is functorial in $\cat{C}$, and this is in fact also true for any family of subsets of $[n]$ by~\cref{cor:simultaneoussafety}.

\section{Applications}\label{sec:applications}
Composable security is a stronger constraint than stand-alone security, and indeed many cryptographic functionalities are known to be impossible to achieve ``in the plain model'', \ie without set-up assumptions. A case in point is bit commitment, which was shown to be impossible in the UC-framework in~\cite{CF01}. This result was later generalized in~\cite{PR08} to show that any two-party functionality that can be realized in the plain UC-framework is ``splittable''. While the authors of~\cite{PR08} remark that their result applies more generally than just to the UC-framework, this wasn't made precise until~\cite{MR11}\footnote{Except that in their framework the 2-party case seems to require security constraints also when both parties cheat.}. We present a categorical proof of this result in our framework, which promotes the pictures ``illustrating the proof'' in~\cite{PR08} into a full proof --- the main difference is that in~\cite{PR08} the pictures explicitly keep track of an environment trying to distinguish between different functionalities, whereas we prove our result in the case of perfect security and then deduce the asymptotic claim.

We now assume that $\C$, our ambient category of interactive computations is compact closed\footnote{We do not view this as overtly restrictive, as many theoretical models of concurrent interactive (probabilistic/quantum) computation are compact closed~\cite{winskel:game,clairambault:gamesforquantum,clairambaultetal:gamesforquantum2}.}. As we are in the 2-party setting, we take our free computations to be given by $\C^2$, and we consider two attack models: one where Alice cheats and Bob is honest, and one where Bob cheats and Alice is honest. We think of $\tinycup$  as representing a two-way communication channel, but this interpretation is not needed for the formal result.
\begin{theorem}\label{thm:bipartite} For Alice and Bob (one of whom might cheat),
if a bipartite functionality $r$ can be securely realized from a communication channel between them, \ie from $\tinycup$, then
\begin{equation}\label{eq:splittable}\tag{$*$}
\text{there is a }g\text{ such that}
\begin{pic}
\node[state] (x) at (0,0) {$r$};
\draw (x.A) to +(0,.4) node[left] {$A$};
\draw (x.B) to +(0,.4) node[right] {$B$};
\end{pic}=\begin{pic}\setlength\morphismheight{3mm}
\setlength\minimummorphismwidth{3mm}
\node[state] (x) at (0,0) {$r$};
\node[state] (y) at (1,0) {$r$};
\node[morphism] (f) at (0.5,0.4) {$g$};
\draw (x.A) node[left] {$$} to +(0,.6);
\draw (x.B) to node[right] {} ([xshift=-4.25pt] f.south west);
\draw (y.A) to node[right] {} ([xshift=4.25pt] f.south east);
\draw (y.B) to  node[right] {$$} +(0,.6);
\end{pic}.
\end{equation}
\end{theorem}
\begin{proof}
If a protocol $(f_A, f_B)$ achieves this, security constraints against each party give us
\[\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (f) at (0,0) {$f_A$};
\draw (f.north) to +(0,.3);
\draw (f.south)  to[out=-90,in=-90] +(.5,0) to +(0,.6);
%\draw (f.south)  to[out=-90,in=-90] +(.5,0) to +(.5,.6); %this for an up-to-date system
\end{pic}=\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (g) at (.225,.35) {$s_B$};
\node[state] (x) at (0,0) {$r$};
\draw (x.A) to +(0,.75) node[right] {};
\draw (g.south) to node[right] {$$} (x.B);
\draw (g.north) to +(0,.25) node[right] {};
\end{pic}
\quad \text{and} \quad\
\begin{pic}[xscale=-1]
\node[morphism,scale=.5,font=\normalsize] (f) at (0,0) {$f_B$};
\draw (f.north) to +(0,.3);
\draw (f.south)  to[out=-90,in=-90] +(.5,0) to +(0,.6);
%\draw (f.south)  to[out=-90,in=-90] +(.5,0) to +(.5,.6); %this for an up-to-date system
\end{pic}=\begin{pic}[xscale=-1]
\node[morphism,scale=.5,font=\normalsize] (g) at (.225,.35) {$s_A$};
\node[state] (x) at (0,0) {$r$};
\draw (x.B) to +(0,.75) node[right] {};
\draw (g.south) to node[right] {$$} (x.A);
\draw (g.north) to +(0,.25) node[right] {};
\end{pic}   \quad \text{so that} \quad\begin{pic}
\node[state] (x) at (0,0) {$r$};
\draw (x.A) to +(0,.3) node[right] {};
\draw (x.B) to +(0,.3) node[right] {};
\end{pic}=\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (f) at (0,0) {$f_A$};
\node[morphism,scale=.5,font=\normalsize] (g) at (.5,0) {$f_B$};
\draw (f.north) to +(0,.3);
\draw (g.north) to +(0,.3);
\draw (f.south)  to[out=-90,in=180] +(0.25,-.25) to[out=0,in=-90] (g.south);
\end{pic}
\node[morphism,scale=.5,font=\normalsize] (f) at (0,0) {$f_A$};
\node[morphism,scale=.5,font=\normalsize] (g) at (1.5,0) {$f_B$};
\draw (f.north) to +(0,.3);
\draw (g.north) to +(0,.3);
\draw (f.south)  to[out=-90,in=-90] +(.5,0) to[out=90,in=180] +(.25,.5) to [out=0,in=90] +(.25,-.5) to [out=-90,in=-90] (g.south);
%\draw (f.south)  to[out=-90,in=-90] +(.5,0) to[out=90,in=180] +(.75,.5) to [out=0,in=90] +(1,0) to [out=-90,in=-90] (g.south);%on an up-to-date-system
\end{pic}
\begin{pic}
\node[morphism,scale=.5,font=\normalsize] (g) at (.23,.35) {$s_B$};
\node[state] (x) at (0,0) {$r$};
\node[morphism,scale=.5,font=\normalsize] (f) at (0.78,.35) {$s_A$};
\node[state] (y) at (1,0) {$r$};
\draw (x.A) to +(0,.75) node[right] {};
\draw (y.B) to +(0,.75) node[right] {};
\draw (g.south) to node[right] {$$} (x.B);
\draw (g.north) to[out=90,in=-180] +(0.275,.25) to [out=0,in=90] (f.north);
\draw (f.south) to node[right] {$$} (y.A);
\end{pic}\qedhere
\]
\end{proof}
\begin{corollary}  Given a compact closed $\C$  modeling  computation in which wires model communication channels, (composable) bit commitment and oblivious transfer are impossible in that model without setup, even asymptotically in terms of distinguisher advantage.
\end{corollary}
\begin{proof}
If $r$ represents bit commitment from Alice to Bob, it does not satisfy the equation required by Theorem~\ref{thm:bipartite} for any $f$, and the two sides of~\eqref{eq:splittable} can be distinguished efficiently with at least probability $1/2$. Indeed, take any $f$ and let us compare the two sides of~\eqref{eq:splittable}: if the distinguisher commits to a random bit $b$, then Bob gets a notification of this on the left hand-side, so that $f$ has to commit to a bit on the right side of~\eqref{eq:splittable} to avoid being distinguished from the left side. But this bit coincides with $b$ with probability at most $1/2$, so that the difference becomes apparent at the reveal stage. The case of OT is similar.
\end{proof}
We now discuss a similar result in the tripartite case, which rules out building a broadcasting channel from pairwise channels securely against any single party cheating. In~\cite{MMP+18} comparable pictures are used to illustrate the official, symbolically rather involved, proof, whereas in our framework the pictures are the proof. Another key difference is that~\cite{MMP+18} rules out broadcasting directly, whereas we show that any tripartite functionality realizable from pairwise channels satisfies some equations, and then use these equations to rule out broadcasting.

Formally, we are working with the resource theory given by $\C^3\xrightarrow{\otimes}\C\xrightarrow{\hom(I,-)}$ where $\C$ is an SMC, and reason about protocols that are secure against three kinds of attacks: one for each party behaving dishonestly while the rest obey the protocol. Note that we do not need to assume compact closure for this result, and the result goes through for any state on $A\otimes A$ shared between each pair of parties: we will denote such a state by $\tinycup$ by convention.

\begin{theorem}  If a tripartite functionality $r$ can be realized from each pair of parties sharing a state
$\tinycup$, securely against any single party, then there are simulators $s_A,s_B,s_C$ such that
\[\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[state] (r) at (0,0) {$r$};
\node[morphism,scale=.5,font=\normalsize] (f) at (-.5,.35) {$s_A$};
\draw ([xshift=-3.5pt]r.A) to (f.south);
\draw ([xshift=3.5pt]r.B) to +(0,.75);
\draw ([xshift=-.5pt]f.north west) to +(0,.25);
\draw ([xshift=.5pt]f.north east) to +(0,.25);
\draw (r.center) to +(0,.75);
\end{pic}\quad=\quad
\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[state] (r) at (0,0) {$r$};
\node[morphism,scale=.5,font=\normalsize] (h) at (0,.35) {$s_B$};
\draw ([xshift=-3.5pt]r.A) to +(0,.75);
\draw ([xshift=3.5pt]r.B) to +(0,.75);
\draw ([xshift=-.5pt]h.north west) to +(0,.25);
\draw ([xshift=.5pt]h.north east) to +(0,.25);
\draw (r.center) to (h.south);
\end{pic}\quad=\quad
\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[state] (r) at (0,0) {$r$};
\node[morphism,scale=.5,font=\normalsize] (g) at (.5,.35) {$s_C$};
\draw ([xshift=-3.5pt]r.A) to +(0,.75);
\draw ([xshift=3.5pt]r.B) to (g.south);
\draw ([xshift=-.5pt]g.north west) to +(0,.25);
\draw ([xshift=.5pt]g.north east) to +(0,.25);
\draw (r.center) to +(0,.75);
\end{pic}\ .
\]
\end{theorem}

\begin{proof}
Any tripartite protocol building on top of each pair of parties sharing $\tinycup$  can be drawn as in the left side of
\[
\begin{pic}
\setlength\morphismheight{3mm}
\node[morphism] (f) at (0,0) {$f_A$};
\node[morphism] (g) at (1,0) {$f_B$};
\node[morphism] (h) at (2,0) {$f_C$};
\draw (f.north) to +(0,.3);
\draw (g.north) to +(0,.3);
\draw (h.north) to +(0,.3);
\draw (f.south east)  to[out=-90,in=-90] (g.south west);
\draw (g.south east)  to[out=-90,in=-90] (h.south west);
\draw (f.south west)  to[out=-90,in=-90] (h.south east);
\end{pic} \qquad\qquad
\begin{pic}
\setlength\morphismheight{3mm}
\coordinate (a) at (0.5,-.9);
\node[morphism] (e) at (-1,0) {$f_A$};
\node[morphism] (f) at (0,0) {$f_B$};
\node[morphism] (g) at (1,0) {$f_B$};
\node[morphism] (h) at (2,0) {$f_C$};
\draw (e.north) to +(0,.3);
\draw (f.north) to +(0,.3);
\draw (g.north) to +(0,.3);
\draw (h.north) to +(0,.3);
\draw (e.south east)  to[out=-90,in=-90] (f.south west);
\draw (f.south east)  to[out=-90,in=-90] (g.south west);
\draw (g.south east)  to[out=-90,in=-90] (h.south west);
\draw (e.south west)  to[out=-90,in=180] (a) to[out=0,in=-90] (h.south east);
\end{pic}
\]
Consider now the morphism in $\C$ depicted on the right: it can be seen as the result of three different attacks on the protocol $(f_A,f_B,f_C)$ in $\C^3$: one where Alice cheats and performs $f_A$ and $f_B$ (and the wire connecting them), one where Bob performs $f_B$ twice, and one where Charlie performs $f_B$ and $f_C$. The security of $(f_A,f_B,f_C)$ against each of these gives the required simulators.
\end{proof}

\begin{corollary}  Given a SMC $\C$ modeling interactive computation, and a state $\tinycup$ on $A\otimes A$ modeling pairwise communication, it is impossible  to build broadcasting channels securely (even asymptotically in terms of distinguisher advantage) from pairwise channels.
\end{corollary}

\begin{proof} We show that a channel $r$ that enables Bob to broadcast an input bit to Alice and Charlie never satisfies the required equations for any $s_A,s_B,s_C$. Indeed,  assume otherwise and let the environment
plug ``broadcast $0$'' and ``broadcast $1$'' to the two wires in the middle. The leftmost picture then says that Charlie receives $1$, the rightmost picture implies that Alice gets $0$ and the middle picture that Alice and Bob get the same output (if anything at all)---a contradiction. Indeed, one cannot satisfy all of these simultaneously with high probability, which rules out an asymptotic transformation.
\end{proof}
\section{Outlook}\label{sec:outlook}

We have presented a categorical formulation of cryptography and thus provided a general, flexible and mathematically robust way of reasoning about composability in cryptography. Besides contributing a further approach to composable cryptography and potentially helping with cross-talk and comparisons between existing approaches~\cite{CKL+19}, we believe that the current work opens the door for several further questions.

First, due to the generality of our approach we hope that one can, besides honest and malicious participants, reason about more refined kinds of adversaries composably. Indeed, we expect that Definition~\ref{def:attack}
is general enough to capture \eg honest-but-curious adversaries\footnote{Heuristically speaking this is the case: an honest-but-curious attack on $g\circ f$ should be factorizable as one on $g$ and one on $f$, and similarly an honest-but-curious attack on $g\otimes f$ should be factorisable into ones on $g$ and~$f$ that then forward their transcripts to an attack on $\id\otimes\id$.}. It would also be interesting to see if this captures even more general attacks, \eg situations where the sets of participants and dishonest parties can change during the protocol. This might require understanding our axiomatization of attack models more structurally and perhaps generalizing it.  Does this structure (or a variant thereof) already arise in category theory? While we define an attack model on a category, perhaps one could define an attack model on a (strong) monoidal functor~$F$, the current definition being recovered when $F=\id$.

Second, we expect that rephrasing cryptographic questions categorically would enable more cross-talk between cryptography and other fields already using category theory as an organizing principle. For instance, many existing approaches to composable cryptography develop their own models of concurrent, asynchronous, probabilistic and interactive computations. As categorical models of such computation exist in the context of game semantics~\cite{winskel:game,clairambault:gamesforquantum,clairambaultetal:gamesforquantum2}, one is left wondering whether the models of the semanticists' could be used to study and answer cryptographic questions, or conversely if the models developed by cryptographers contain valuable insights for programming language semantics.

Besides working inside concrete models---which ultimately blends into ``just doing composable cryptography''---one could study axiomatically how properties of a category relate to cryptographic properties in it. As a specific conjecture in this direction, if one has an environment structure~\cite{coecke:environment}, \ie coherent families of maps $\tinyground_A$ for each $A$ that axiomatize the idea of deleting a system, one might be able to talk about honest-but-curious adversaries at an abstract level. Similarly, having agents purify their actions is an important tool in quantum cryptography~\cite{LC97}---can categorical accounts of purification~\cite{chiribella:purification,cunningham:purity,coecke:environment} be used to elucidate this?

Finally, we hope to get more mileage out of the tools brought in with the categorical viewpoint. For instance, can one prove further no-go results pictorially? More specifically, given the impossibility results for two and three parties, one wonders if the ``only topology matters'' approach of string diagrams can be used to derive general impossibility results for $n$ parties sharing pairwise channels. Similarly, while diagrammatic languages have been used to reason about positive cryptographic results in the stand-alone setting~\cite{kissinger2017picture,breiner:graphicaldicrypto,breiner:selftesting}, can one push such approaches further now that composable security definitions have a clear categorical meaning? Besides the graphical methods, thinking of cryptography as a resource theory suggests using resource-theoretic tools such as monotones. While monotones have already been applied in cryptography~\cite{WW08:monotones}, a full understanding of cryptographically relevant monotones is still lacking.

\bibliography{bib/full,bib/quantum,new,new2}

\appendix
\section{Background}\label{sec:background}

\subsection{Monoidal categories and string diagrams}\label{sec:pictures}

We assume that the reader is familiar with category theory in general and with  monoidal and compact closed categories in particular, so we will briefly recall the main concepts, mostly to explain the notation and string diagrams used. General references for category theory include~\cite{maclane:categories,awodey:categorytheory,borceux:vol1,borceux:vol2,riehl:categorytheory,leinster:basicCT} and string diagrams are surveyed in~\cite{Sel10}. However, a working cryptographer might find it easier to consult texts which are written with some applications in mind and introduce string diagrams concurrently with categories, such as~\cite{coecke2010categories,FS19,heunenvicary:categories}.

Let $\C$ be a symmetric monoidal category (SMC). Roughly speaking, this means that we have a class of objects $A,B,C,\dots$, and a class of morphisms $f,g,h,\dots$. We also have functions $\dom$ and $\cod$ that give us the domain and codomain of morphisms, and we write $f\colon A\to B$ to express that $A=\dom(f)$ and $B=\cod(f)$. Morphisms can be composed sequentially, \ie whenever $f\colon A\to B$ and $g\colon B\to C$ there is a morphism $g\circ f=gf\colon A\to C$. In addition, there is a monoidal product $\otimes$ on objects and morphisms, that sends $f\colon A\to B$ and $g\colon C\to D$ to $f\otimes g\colon A\otimes C\to B\otimes D$. For each object there should be an identity morphism $\id[A]\colon A\to A$, and there should be a special object $I$ called the tensor unit. This data is subject to some constraints: composition should be (strictly) associative and unital, and the monoidal product should be associative, commutative and unital \emph{up to coherent isomorphisms}, see~\cite[Section 6.1]{borceux:vol2} for the precise details. Moreover, $\circ$ and $\otimes$ should cooperate in that the equations $(g\circ f)\otimes (j\circ h)=(g\otimes j)\circ (f\otimes h)$ and $\id[A\otimes B]=\id[A]\otimes \id[B]$ hold. We will assume throughout that the variables $\C$ and~$\D$ denote strict SMCs, meaning that associativity and unitality of $\otimes$ holds up to equality. This is mainly for notational convenience---first, any SMC is equivalent to a strict one and second, the theory we put forward could be developed without assuming strictness at the cost of some notational overhead. As an example of a (non-strict) SMC the reader could think \eg of the category $\Set$ of sets and functions between them, with the monoidal structure given by cartesian product, or the category $\cat{Vect}_\mathbb{R}$ of real vector spaces and linear maps between them, with the monoidal structure given by tensor product.

The tersely sketched structure of a SMC is naturally internalized in the \emph{graphical calculus} we  use, which provides a sound and complete method for reasoning about them. Thus the reader less familiar with SMCs is invited to trust their visual intuition as it is unlikely to lead them astray. In this graphical calculus, we will denote a morphism $f\colon A\to B$ as $\begin{pic}
\node[morphism,font=\tiny] (f) at (0,0) {$f$};
\draw (f.south) to +(0,-.1)  node[right] {$A$};
\draw (f.north) to +(0,.1)  node[right] {$B$};
\end{pic}$, and composition and monoidal product as
\[
\begin{pic}
\node[morphism] (f) {$g \circ f$};
\draw (f.south) to +(0,-.65) node[right] {$A$};
\draw (f.north) to +(0,.65) node[right] {$C$};
\end{pic}
\begin{pic}
\node[morphism] (g) at (0,.75) {$g\vphantom{f}$};
\node[morphism] (f) at (0,0) {$f$};
\draw (f.south) to +(0,-.3) node[right] {$A$};
\draw (g.south) to node[right] {$$} (f.north);
\draw (g.north) to +(0,.3) node[right] {$C$};
\end{pic}
\qquad\qquad
\begin{pic}
\node[morphism] (f) {$f \otimes g$};
\draw (f.south) to +(0,-.65) node[right] {$A \otimes C$};
\draw (f.north) to +(0,.65) node[right] {$B \otimes D$};
\end{pic}
\begin{pic}
\node[morphism] (f) at (-.4,0) {$f$};
\node[morphism] (g) at (.4,0) {$g\vphantom{f}$};
\draw (f.south) to +(0,-.65) node[right] {$A$};
\draw (f.north) to +(0,.65) node[right] {$B$};
\draw (g.south) to +(0,-.65) node[right] {$C$};
\draw (g.north) to +(0,.65) node[right] {$D$};
\end{pic}
\]
Special morphisms get special pictures: identities and symmetries are depicted as
\[\begin{pic}
\draw (0,0) node[right] {$A$} to (0,1) node[right] {$A$};
\end{pic}
\qquad\qquad\qquad
\begin{pic}
\draw (0,0) node[left] {$A$} to[out=80,in=-100] (1,1) node[right] {$A$};
\draw (1,0) node[right] {$B$} to[out=100,in=-80] (0,1) node[left] {$B$};
\end{pic}
\]
whereas the identity on the tensor unit is denoted by the empty picture. In general, a morphism might have multiple input/output wires
\[
\begin{pic}
\node[morphism] (f) at (0,0) {$f$};
\node (a) at (0,.5) {$\ldots$};
\node (b) at (0,-.5) {$\ldots$};
\draw ([xshift=-2.5pt]f.south west) to +(0,-.5) node[left] {$A_1$};
\draw ([xshift=-2.5pt]f.north west) to +(0,.5) node[left] {$B_1$};
\draw ([xshift=2.5pt]f.south east) to +(0,-.5) node[right] {$A_n$};
\draw ([xshift=2.5pt]f.north east) to +(0,.5) node[right] {$B_m$};
\end{pic}\]
In particular a morphism $I\to A_1\otimes\dots\otimes A_n$ will have no incoming wires. We will call such morphisms \emph{states} on $A_1\otimes\dots\otimes A_n$ and depict them as triangles instead of boxes:
\[
\begin{pic}
\node[state] (f) at (0,0) {$f$};
\node (a) at (0,.25) {$\ldots$};
\draw ([xshift=-1.5pt]f.A) to +(0,.5) node[left] {$A_1$};
\draw ([xshift=1.5pt]f.B) to +(0,.5) node[right] {$A_n$};
\end{pic}
\]
Note that the property $\id[A\otimes B]=\id[A]\otimes \id[B]$ becomes
\[\begin{pic}
\draw (0,0) node[right] {$A\otimes B$} to (0,1) node[right] {$A\otimes B$};
\end{pic}
\qquad=\qquad
\begin{pic}
\draw (0,0) node[left] {$A$} to (0,1) node[left] {$A$};
\draw (1,0) node[right] {$B$} to (1,1) node[right] {$B$};
\end{pic}
\]
so that whether multiple wires are packaged into one or not is largely a matter of convenience. We  will often omit labeling wires with the name of the object unless necessary, and at times the label will only give partial information.

For Theorem~\ref{thm:bipartite} we will assume that our ambient category~$\C$ is in fact a \emph{compact closed category}. This means that $\C$ is an SMC, and we are also given for every object $A$ an object $A^*$ and morphisms
\[
\begin{pic}[yscale=-1]
\draw (0,1) node[left] {$A^*$} to[out=90,in=180] (.5,1.5);
\draw (.5,1.5) to[out=0,in=90] (1,1)  node[right] {$A$};
\end{pic}
\quad \text{and}\quad
\begin{pic}
\draw (0,1) node[left] {$A$} to[out=90,in=180] (.5,1.5);
\draw (.5,1.5)  to[out=0,in=90] (1,1) node[right] {$A^*$};
\end{pic},
\]
called cups and caps respectively, satisfying
\[
\begin{pic}
\draw (0,0) to (0,1) to[out=90,in=180] (.5,1.5);
\draw (.5,1.5) to[out=0,in=90] (1,1) to[out=-90,in=180] (1.5,.5);
\draw (1.5,.5) to[out=0,in=-90] (2,1) to (2,2);
\end{pic}
\quad = \quad \begin{pic}
\draw (0,0) node[right] {$A$} to (0,2) node[right] {$A$};
\end{pic}
\text{and}
\quad
\begin{pic}[xscale=-1]
\draw (0,0) to (0,1) to[out=90,in=180] (.5,1.5);
\draw (.5,1.5) to[out=0,in=90] (1,1) to[out=-90,in=180] (1.5,.5);
\draw (1.5,.5) to[out=0,in=-90] (2,1) to (2,2);
\end{pic} \quad=\quad
\begin{pic}
\draw (0,0) node[right] {$A^*$} to (0,2) node[right] {$A^*$};
\end{pic}
\]
Informally, this somewhat blurs the distinction between input and output wires, as one expects to happen if the boxes represent interactive and open computational processes. In particular, morphisms $A\to B$ correspond bijectively to states on $A^*\otimes B$, where the bijection is given by bending and unbending wires, and this correspondence should be seen as the categorical counterpart to the Choi–Jamio\l{}kowski isomorphism from quantum information.

We will briefly conclude this section by discussing functors between SMCs. A lax monoidal functor $\cat{C}\to\cat{D}$ between monoidal categories is a functor $F\colon\cat{C}\to\cat{D}$ equipped with natural maps $F(A)\otimes F(B)\to F(A\otimes B)$ and a morphism $I_\cat{D}\to F(I_\C)$ subject to certain coherence equations that roughly say that it cooperates with the monoidal structures on $\cat{C},\cat{D}$ in a well-behaved manner. A strong monoidal functor is a lax monoidal one for which the structure maps $F(A)\otimes F(B)\to F(A\otimes B)$ and $I_\cat{D}\to F(I_\C)$ are isomorphisms. A monoidal functor (in either sense) is symmetric if it additionally cooperates with the symmetries. We will use graphical calculus of strong monoidal functors in the proof of Theorem~\ref{thm:perfectlifting}, but otherwise do not refer to the detailed definitions nor use this graphical language, and hence we do not go into more detail here. Full definitions can be found \eg at~\cite[Section I.1.2]{leinster2004} or at~\cite[Section 6.4]{borceux:vol2}, and a graphical calculus for them is discussed in~\cite{mellies2006functorial}. For us, all functors will be symmetric and either strong or lax monoidal, and we will specify which we mean whenever it makes a difference.

\section{Proofs of Theorems~\ref{thm:composition} and \ref{thm:perfectlifting}}\label{sec:proofs}

\composition*

\begin{proof}
We first prove the claim when $F=\id[\C]$. As the class of  $\A$-secure maps is a subclass of maps inside an SMC, it suffices to show it contains all coherence isomorphisms (and thus all identities) and is closed under $\circ$ and $\otimes$.

For coherence isomorphisms we prove a stronger claim and show that all isomorphisms are $\A$-secure. Let $f\colon (A,r)\to (B,s)$ be an isomorphism so that $f$ is an isomorphism $A\to B$ in $\cat{C}$, and consider $f'\in \A(f)$ with $\dom(f')=A$. Then $R(f')r=R(f')R(f^{-1})R(f)r=R(f')R(f^{-1})s$, so it suffices to show that $f'f^{-1}\in\A(\id[B])$. Property (i) of $\A$ implies that $(f^{-1})\in\A(f^{-1})$ so that property $(ii)$ gives us $f'f^{-1}\in\A(ff^{-1})=\A(\id[B])$, as desired.

Assume now that  $f\colon (A,r)\to (B,s)$ and $g\colon (B,s)\to (C,t)$ are $\A$-secure. Given $h\in\A(g\circ f)$ with domain $A$, factorize it as $g'\circ f'$ as guaranteed by (ii). As $f$ is $\A$-secure, there is some $b\in \A(\id[B])$ with $R(f')r=R(b)s$  and  thus $g'b\in\A(g)$ by (ii) so that security of $g$ implies the existence of $c\in\A(\id[B])$ such that $R(g'b)(s)=R(c)t$. Thus $R(g'f')t=R(g')R(b)s=R(c)t$ showing that $g\circ f$ is $\A$-secure.

To show that secure maps are closed under $\otimes$, let  $f\colon (A,r)\to (B,s)$ and $g\colon (C,t)\to (D,u)$ be $\A$-secure. Given $h\in \A(f\otimes g)$ with domain $A\otimes C$, factorize it as $h'\circ (f'\otimes g')$ as guaranteed by (iii). Then security of $f$ and $g$ gives us $b\in\A(\id[B])$ and $d\in\A(\id[D])$ so that $R(f')r=R(b)s$ and $R(g')t=R(d)u$. This implies that $R(h)(r\otimes t)=R(h')\circ (R(b)\otimes R(d))(s\otimes u)$, so $h'\circ (b\otimes d)\in \A(\id[B]\otimes\id[D])$ witnesses that $f\otimes g$ is $\A$-secure.

To prove the claim for an arbitrary strong monoidal~$F$, observe first that $f\colon (A,r)\to (B,s)$ is $\A$-secure if, and only if $F(f)\colon (F(A),r)\to (F(B),s)$ is $\A$-secure. The claim can now be deduced from the existence and description of pullbacks in the category of SMCs, but  we give an explicit proof: the class of $\A$-secure maps in $\res RF$  contains all isomorphisms and is closed under composition because it is so in $\res R$. As~$F$ is strong monoidal, the square
\[\begin{tikzpicture}
\matrix (m) [matrix of math nodes,row sep=2em,column sep=4em,minimum width=2em]
F(A\otimes C) & F(B\otimes D) \\
F(A)\otimes F(C) & F(B)\otimes F(D) \\};
\path[->]
(m-1-1) edge node [left] {$\cong$} (m-2-1)
edge node [above] {$F(f\otimes g)$} (m-1-2)
(m-2-2) edge node [right] {$\cong$} (m-1-2)
(m-2-1) edge node [below] {$F(f)\otimes F(g)$}  (m-2-2);
\end{tikzpicture}\]
commutes in $\C$. If $f\colon (A,r)\to (B,s)$ and $g\colon (C,t)\to (D,u)$ are $\A$-secure in $\res RF$, then $F(f)$ and $F(g)$ are $\A$-secure in $\res R$. The case $F=\id[\C]$  implies that $F(f)\otimes F(g)$ is $\A$-secure so that $F(f\otimes g)$ is $\A$-secure as a composite of secure maps, which means that $f\otimes g$ is $\A$-secure in $\res RF$ as desired.
\end{proof}

\perfectlifting*

\begin{proof}
Let us first spell out explicitly how the domain and codomain of $(Ff_1,\dots,Ff_n)$ depends on those of $\f$: if $\bar{f}\colon ((A_i)_{i=1}^n,r)\to ((B_i)^n_{i=1},s)$, then $Fr\colon F(I_\C)\to F(\bigotimes_{i=1}^n A_i)$ induces a state on $\bigotimes_{i=1}^n F(A_i)$ by precomposing with the isomorphism $I_\D\to F(I_\C)$ and postcomposing with the isomorphism $F(\bigotimes_{i=1}^n A_i)\cong \bigotimes_{i=1}^n F(A_i)$ stemming from the strong monoidal structure of $F$. This is the state that $(Ff_1,\dots,Ff_n)$ transforms to the one induced by $F(s)$. Let us now show that this transformation is secure provided that $\f$ is.

The heart of the argument is already apparent in the case of $n=2$, so let us first show that if $(f_A,f_B)$ is secure against a malicious Bob, so is $(Ff_A,Ff_B)$.  For this attack model, there is an initial attack, and the corresponding security constraint is depicted in~\cref{fig:initial_attack}. Then security of $(Ff_A,Ff_B)$ can be shown graphically using the functorial boxes of~\cite{mellies2006functorial} by considering the equations
\[
\begin{pic}
\node at (.8,-.6) {$F$};
\setlength\minimumstatewidth{15mm}
\node[nmorphismtwocell,scale=.5,font=\normalsize] (f) at (-.5,.5) {$f_{A}$};
\node[state] (x) at (0,0) {$r$};
\draw (f.south) to node[left] {$A$} ([xshift=-3.5pt]x.A);
\draw (f.north) to +(0,.6) node[right] {};
\draw ([xshift=3.5pt]x.B) to node[right]  {$B$} +(0,.35)  to +(0,1.25);
\draw[black, fill = blue, fill opacity = 0.5, semithick] (-.9,-.75) to (-.9,1.3)
to (-0.2,1.3) to +(0,-1) to[in=-90,out=-90] +(0.4,-1) to +(0,1) %to (-0.2,1.3) to +(0,-1) to[in=-90,out=-90] +(0.4,-1) to +(0.4,0)  if up-to-date
to (.9,1.3) to (.9,-.75) to (-.9,-.75);
\end{pic}=
\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[nmorphismtwocell,scale=.5,font=\normalsize] (f) at (-.5,.5) {$f_{A}$};
\node[state] (x) at (0,0) {$r$};
\draw (f.south) to node[left] {$A$} ([xshift=-3.5pt]x.A);
\draw (f.north) to +(0,.6) node[right] {};
\draw ([xshift=3.5pt]x.B) to node[right]  {$B$} +(0,.35)  to +(0,1.25);
\draw[black, fill = blue, fill opacity = 0.5, semithick] (-.9,-.75) to (-.9,1.3)
to (-0.2,1.3) to +(0,-.4) to[in=-90,out=-90] +(0.4,-.4) to +(0,0.4) %to (-0.2,1.3) to +(0,-.4) to[in=-90,out=-90] +(0.4,-.4) to +(0.4,0)  if up-to-date
to (.9,1.3) to (.9,-.75) to (-.9,-.75);
\node at (.8,-.6) {$F$};
\end{pic}=\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[nmorphismtwocell,scale=.5,font=\normalsize] (g) at (.5,.5) {$b$};
\node[state] (x) at (0,0) {$s$};
\draw ([xshift=-3.5pt]x.A) to node[left] {$A$} +(0,.35) to +(0,1.25);
\draw (g.south) to node[right] {$B$} ([xshift=3.5pt]x.B);
\draw (g.north) to +(0,.6) node[right] {};
\draw[black, fill = blue, fill opacity = 0.5, semithick] (-.9,-.75) to (-.9,1.3)
to (-0.2,1.3) to +(0,-.4) to[in=-90,out=-90] +(0.4,-.4) to +(0,0.4) %to (-0.2,1.3) to +(0,-.4) to[in=-90,out=-90] +(0.4,-.4) to +(0.4,0)  if up-to-date
to (.9,1.3) to (.9,-.75) to (-.9,-.75);
\node at (.8,-.6) {$F$};
\end{pic}
\begin{pic}
\setlength\minimumstatewidth{15mm}
\node[nmorphismtwocell,scale=.5,font=\normalsize] (g) at (.5,.5) {$b$};
\node[state] (x) at (0,0) {$s$};
\draw ([xshift=-3.5pt]x.A) to node[left] {$A$} +(0,.35) to +(0,1.25);
\draw (g.south) to node[right] {$B$} ([xshift=3.5pt]x.B);
\draw (g.north) to +(0,.6) node[right] {};
\draw[black, fill = blue, fill opacity = 0.5, semithick] (-.9,-.75) to (-.9,1.3)
to (-0.2,1.3) to +(0,-1) to[in=-90,out=-90] +(0.4,-1) to +(0,1) %to (-0.2,1.3) to +(0,-1) to[in=-90,out=-90] +(0.4,-1) to +(0.4,0) if up-to-date
to (.9,1.3) to (.9,-.75) to (-.9,-.75);
\node at (.8,-.6) {$F$};
\end{pic}
\]
where the second equation is security of the original protocol and the other two equations rely on $F$ being strong monoidal. The case of an arbitrary $n$ can be shown similarly by drawing a similar picture with $n-1$ dips in the box.
\end{proof}

\section{Further extensions of the framework}

\subsection{Approximately correct transformations}\label{sec:metric}

The discussion above has been focused on perfect security, so that the equations defining security hold exactly. This is often too high a standard for security to hope for, and consequently cryptographers routinely work with computational or approximate security. We model this in two ways. The first approach replaces equations with an equivalence relation abstracting from the idea that the end results are ``computationally indistinguishable'' rather than strictly equal. The latter approach amounts to working in terms of a (pseudo)metric, that quantifies how close we are to the ideal resource, so that one can discuss approximately correct transformations or sequences of transformations that succeed in the limit. The first approach is mathematically straightforward and we discuss it next, while the second approach takes the rest of this section. The second approach, while mathematically more involved, is needed to model protocols that are ``close enough'' to being computationally indistinguishable from the ideal, and thus to model statements in finite-key cryptography~\cite{TLGR12}.

Replacing strict equalities with equivalence relations is easy to describe on an abstract level as an instance of the theory so far: one just assumes that $\C$ has a monoidal congruence $\approx$ and then works with the resource theory induced by $\C^n\to\C/{\approx}\xrightarrow{\hom(I,-)}\Set$ with similar attack models as above. More explicitly, as long as each hom-set of $\C$ is equipped with an equivalence relation $\approx$ that respects $\otimes$ and $\circ$ in that $f\approx f'$ and $g\approx g'$ imply $gf\approx g'f'$ (whenever defined) and $g\otimes f\approx g'\otimes f'$, then working with $\C^n\to\C/{\approx}\xrightarrow{\hom(I,-)}\Set$ results in security conditions that replace $=$ in $\C$ with $\approx$ throughout. If $\C$ describes (interactive) computational processes and $\approx$ represents computational indistinguishability (inability for any ``efficient'' process to distinguish between the two), one might need to replace $\C$ (and consequently functionalities, protocols and attacks on them) with the subcategory of $\C$ of efficient processes so that $\approx$ indeed results in a congruence.

We now move to the metric case. If for each $A$ the set of resources $R(A)$ associated  to it is not just a set but has the structure of a metric space, using this additional structure enables one to construct other resource theories where instead of transforming $r\in R(A)$ to $s\in R(B)$ exactly we are happy to be able to get (arbitrarily) close. While such approximate (or asymptotic) conversions are readily studied in the physics literature (see~\eg~\cite[V.A and V.B]{chitambar:resource}), as far as we are aware this has not been formalized in the categorical context, so we first describe the situation without security constraints. As many interesting measures of distance in cryptography are in fact pseudometrics (non-equal functionalities might have distance~$0$), we work in a more general setting.

\begin{definition}
An \emph{extended pseudometric space} is a pair $(X,d)$ where $X$ is a set and $d\colon X\times X\to [0,\infty]$ is a function satisfying  (i) $d(x,x)=0$, (ii) $d(x,y)=d(y,x)$ and (iii) $d(x,z)\leq d(x,y)+d(y,z)$ for all $x,y,z\in X$. A \emph{short map} $(X,d)\to (Y,e)$ is a function $f\colon X\to Y$ satisfying $d(x,y)\geq e(f(x),f(y))$. We will denote the category of extended pseudometric spaces and short maps simply by $\Met$. We equip $\Met$ with a monoidal structure where $(X,d)\otimes (Y,e)$ is given by equipping $X\times Y$ with $\ell^1$-distance, \ie the distance between $(x,y)$ and $(x',y')$ is given by $d(x,x')+e(y,y')$.

Let $R\colon \cat{C}\to\Met$ be a symmetric monoidal functor. Given $r\in R(A)$, $s\in R(B)$ and $\epsilon>0$, a morphism $f\colon A\to B$ is an \emph{$\epsilon$-correct transformation $(A,r)\to (B,s)$} if $d(R(f)r,s)<\epsilon$. The resource theory $\resmet R$ of \emph{asymptotically correct conversions} is defined as follows: an object is given by a pair $(A,r)$ where $A$ is an object of $\C$ and $r\in R(A)$. A morphism $(A,r)\to (B,s)$ is given by a sequence $(f_n)_{n\in\N}$ of maps $A\to B$ in $\C$  that is eventually $\epsilon$-correct for any $\epsilon>0$, \ie for which $R(f_n)r\to s$ as $n\to\infty$.
\end{definition}

In some resource theories, the relevant asymptotic transformations are allowed to use more and more copies of the resource, so that instead of a sequence  of maps $A\to B$ we have a sequence $(f_n)_{n\in\N}$ of maps $A^{\otimes n}\to B$ taking $r^{\otimes n}$ to~$s$ in the limit. The theory developed here adapts easily to this variant as well, with essentially the same proofs.

\begin{lemma}\label{lem:epsiloncorrect}
Let $R\colon \cat{C}\to\Met$ be symmetric monoidal. The composite (tensor product) of an $\epsilon$-correct map with an $\epsilon'$-correct map is $\epsilon+\epsilon'$-correct.
\end{lemma}

\begin{proof}
Assume that $f$ is an $\epsilon$-correct transformation $(A,r)\to (B,s)$ and that $g$ is an $\epsilon'$-correct transformation $(B,s)\to (C,t)$. As  $R(g)$ is a short map, this gives $d(R(gf)r,s)\leq d(R(gf)r,R(g)s)+d(R(g)s,t)<\epsilon+\epsilon'$.

Assume now that $f:(A,r)\to (B,s)$ is a $\epsilon$-correct and that $g\colon(C,t)\to (D,u)$ is $\epsilon'$-correct. Then $d(R(f\otimes g)r\otimes t,s\otimes u)\leq d((R(f)s,R(g)t),(s,u))=d(R(f)r,s)+d(R(g)t,u)<\epsilon+\epsilon'$.\looseness=-1
\end{proof}

\begin{theorem}
The resource theory $\resmet R$ of asymptotically correct conversions induced by $R\colon \cat{C}\to\Met$ is a symmetric monoidal category.
\end{theorem}

\begin{proof}
The coherence isomorphisms are given by constant sequences of coherence isomorphisms of the resource theory induced by $\cat{C}\xrightarrow{R}\Met\to\Set$, and this implies that they satisfy the required equations of a SMC. Moreover, as they are exact resource conversions, they are also asymptotically correct. Thus it suffices to check that asymptotically correct conversions are closed under $\circ$ and $\otimes$. But this follows from Lemma~\ref{lem:epsiloncorrect}: given two asymptotically correct transformations and $\epsilon>0$, the two transformations are eventually $\epsilon/2$-correct after which their composite (whether $\circ$ or $\otimes$) is $\epsilon$-correct.
\end{proof}

In particular, if $\C$ is $\Met$-enriched, the functor $\hom(I,-)$ lands in $\Met$ so that one can discuss asymptotic transformations between states.

While in resource theories one first tries to understand whether a given transformation is possible at all, once some resource conversion has been shown to be possible one might ask for more. In particular, in the asymptotic setting one might want the sequence $(f_n)_{n\in \N}$ to be efficient (and in particular computable) in $n$, and to converge to the target fast in terms of some measure of cost of implementing $f_n$. One might even want to be able to give an explicit bound on the distance between $R(f_n)r$ and $s$, as is done for instance in finite-key cryptography~\cite{TLGR12}.
However, such considerations are best addressed when working inside a specific resource theory rather than being hardwired into the definitions at the abstract level. Conversely, if one can show that a given asymptotic transformation is impossible even for such a permissive notion of transformation, the resulting no-go theorem is stronger than if one worked with ``efficient'' sequences.

\subsection{Computational security}\label{sec:computationalsecurity}

We now show that one can reason composably about computational security in such a metric setting. The proofs follow rather straightforwardly from the definitions we have by using the structure at hand: most importantly, from the triangle inequality of any metric space and the fact that our maps between metric spaces are contractive. For concrete models of cryptography, one might need to do nontrivial work to show that one has all this structure, after which our theorems apply.

\begin{definition}
Consider  $F\colon\cat{D}\to\cat{C}$ and $R\colon \cat{C}\to\Met$ and an attack model $\A$ on $\cat{C}$. For an $\epsilon>0$ and an $\epsilon$-correct map $(A,r)\to (B,s)$, we say that $f$ is an \emph{$\epsilon$-secure transformation} $(A,r)\to (B,s)$ against $\A$ if for any  $f'\in \A(F(f))$ with $\dom(f')=F(A)$ there is $b\in\A(\id[F(B)])$ such that $d(R(f')r,R(b)s)<\epsilon$.

Let $(f_n)_{n\in\N}\colon (A,r)\to (B,s)$ now define an asymptotically correct conversion in $\resmet RF$. We say that $(f)_{n\in\N}$ is \emph{asymptotically secure} against $\A$ (or asymptotically $\A$-secure) if  it is eventually $\epsilon$-secure for any $\epsilon>0$. Explicitly, $(f_n)_{n\in\N}\colon (A,r)\to (B,s)$ is asymptotically secure if for any $\epsilon>0$ there is a threshold $k\in\N$ such that for any $n>k$ and any $f'\in \A(F(f_n))$ with $\dom(f')=F(A)$ there is $b\in\A(\id[F(B)])$ such that $d(R(f')r,R(b)s)<\epsilon$.
\end{definition}

We now show that bounds on security compose additively.

\begin{lemma}\label{lem:epsilonsafe} Let $R\colon \cat{C}\to\Met$ be lax monoidal and $\A$ an attack model on $\C$. The composite (tensor product) of an $\epsilon$-secure map with an $\epsilon'$-secure map is $\epsilon+\epsilon'$-secure.
\end{lemma}

\begin{proof}
We have already seen that $\epsilon$-correctness behaves as desired in Lemma~\ref{lem:epsiloncorrect}. Assume that $f$ is an $\epsilon$-secure transformation $(A,r)\to (B,t)$ and that $g$ is an $\epsilon'$-secure transformation $(B,s)\to (C,t)$ against $\A$. Given $h\in\A(g\circ f)$ with domain~$A$, factorize it as $g'\circ f'$ as guaranteed by (ii).
As $f$ is $\A$-secure there is some $s\in \A(\id[B])$ with $d(R(f')r,R(b)s)<\epsilon$.  Now $g'b\in\A(g)$ by (ii) so that security of $g$ implies the existence of $c\in\A(\id[B])$ such that $d(R(g'b)(s),R(c)t)<\epsilon'$. Thus $d(R(g'f')t,R(c)t)\leq d(R(g'f')t,R(g')R(b)s)+ d(R(g')R(b)s,R(c)t)<\epsilon+\epsilon'$ as desired.

Assume now that  $f$ is $\epsilon$-secure transformation $(A,r)\to (B,t)$ against $\A$ and that $g$ is $\epsilon'$-secure transformation $(C,t)\to (D,u)$ against $\A$.  Given $h\in \A(f\otimes g)$ with domain $A\otimes C$ factorize it as $h'\circ (f'\circ g')$ as guaranteed by (iii). Then $\epsilon$-security of $f$ ($\epsilon'$-security of $g$) gives us $b\in\A(\id[B])$ so that $d(R(f')r,R(b)s)<\epsilon$ ($d\in\A(\id[D])$ so that $d(R(g')t,R(d)u)<\epsilon'$). Now $d(R(h')\circ R(f'\otimes g')(r\otimes t),R(h')\circ (R(b)\otimes R(d))(s\otimes u))\leq d(R(f'\otimes g')(r\otimes t),(R(b)\otimes R(d))(s\otimes u))=d(R(f')r,R(b)s)+d(R(g')t,R(d)u<\epsilon+\epsilon'$ as desired.
\end{proof}

We now give a composition theorem for asymptotically secure protocols.

\begin{theorem}\label{thm:metriccomposition}
Given symmetric monoidal functors $F\colon\cat{D}\to\cat{C}$,  $R\colon \cat{C}\to\Set$ with $F$ strong monoidal and $R$ lax monoidal, and an attack model $\A$ on $\cat{C}$, the class of asymptotically $\A$-secure maps forms a wide sub-SMC of the asymptotic resource theory $\resmet RF$ induced by $F$ and $R$.
\end{theorem}

\begin{proof}
As with Theorem~\ref{thm:composition}, it suffices to show that asymptotically secure maps contain all coherence isomorphisms and are closed under $\circ$ and $\otimes$. Moreover, the reduction from the general case to $F=\id$ is the same, so we assume that $F=\id$.
It is easy to see that whenever $f$ is $\A$-secure in the resource theory induced by $\cat{C}\xrightarrow{R}\Met\to\Set$, the constant sequence  $(f)_{n\in \N}$ is asymptotically $\A$-secure. Thus security of coherence isomorphisms implies their asymptotic security.

Assume now that  $(f_n)_{n\in \N}\colon (A,r)\to (B,s)$ and $(g_n)_{n\in \N}\colon (B,s)\to (C,t)$ are asymptotically $\A$-secure. Given $\epsilon>0$, for sufficiently large $n$ both $f_n$ and $g_n$ are $\epsilon/2$-secure so that their composite is $\epsilon$-secure by Lemma~\ref{lem:epsilonsafe}. The case for~$\otimes$ follows similarly from Lemma~\ref{lem:epsilonsafe}.
\end{proof}

\begin{corollary}\label{cor:metricsimultaneoussafety}
Given a non-empty family of functors $(\cat{D}\xrightarrow{F_i}\cat{C_i}\xrightarrow{R_i}\Met)_{i\in I}$ with  $R:=R_iF_i=R_jF_j$ for all $i,j\in I$  and attack models $\A_i$ on $\C_i$ for each $i$, the class of maps in $\resmet R$ that is asymptotically secure against each $\A_i$ is a sub-SMC of $\resmet R$.
\end{corollary}

To make these abstract results closer to cryptographic practice, one would work within some explicit $\C$ and with (pseudo)metrics relevant for cryptographers. A paradigmatic case is given by metrics induced by distinguisher advantage, where one defines the distance between two behaviors as the supremum over all (efficient) distinguishers $d$ of the probability of $d$ distinguishing the two behaviors. If our starting category $\C$ contains processes that are not (efficiently) computable, such distinguisher metrics might not be contractive as composing two distinct behaviors with a very powerful behavior might help a distinguisher trying to tell them apart. However, as long as
one restricts~$\C$ (and consequently the behaviors available as resources, protocols and attacks) to behaviors that the relevant class of distinguishers can freely implement, this readily results in a $\Met$-enrichment, as composing two morphisms with a fixed morphism available to the distinguishers cannot increase distinguisher advantage. For instance, if the metric is induced by distinguisher advantage of polynomial-time distinguishers, one should get a $\Met$-enrichment on the subcategory of $\C$ corresponding to polynomial-time behaviors.  Once one has specified a concrete~$\C$ and a $\Met$-enrichment on it, for any asymptotically secure protocol one can then discuss its speed of convergence, and in principle discuss which actual value of the security parameter is sufficiently secure for the task at hand.

We now wish to prove a variant of Theorem~\ref{thm:perfectlifting} in the approximate setting, abstracting from~\cite[Theorem 18]{Unr10}. Again, we specialize to the $n$-partite resource theory of states, where our attack models consist of some subset $J\subset\{1,\dots,n\}$ behaving maliciously. In this case, we assume our base categories to be $\Met$-enriched, so that $\hom(I,-)$ lands in $\Met$. In such a setting, a protocol is a sequence $(\f_i)_{i\in\N}$ where each $\bar{f_i}:=(f_{i,1},\dots f_{i,n})$ is an $n$-tuple of morphisms.

\begin{theorem}\label{thm:computationallifting}
Let $\cat{C}$ and $\cat{D}$ be $\Met$-enriched SMCs, and let $F\colon \cat{C}\to\cat{D}$ be a strong monoidal $\Met$-enriched functor. If $(\f_i)_{i\in\N}$ is an asymptotic transformation between two states of $\cat{C}$ that is asymptotically secure against $J\subset\{1,\dot n\}$, so is $(F\f_i)_{i\in \N}$.
\end{theorem}

\begin{proof}
Again, it suffices to prove security against initial attacks. Now, the proof of~\cref{thm:perfectlifting} implies that if the desired equation in $\C$ holds up to $\epsilon>0$, so does the equation in $\D$, so the claim follows.
\end{proof}

As discussed in~\cite{Unr10}, the computational version above is not as strong as the result in the case of perfect security, as the assumptions of Theorem~\ref{thm:computationallifting} are rather strong. For instance, if a protocol is secure against polynomial-time classical adversaries, it does not follow that it is secure against polynomial-time quantum adversaries. Correspondingly, if we use the metric induced by ``polynomial-time distinguishers'', the inclusion of classical computations into quantum computations is not $\Met$-enriched, as the distances might increase. However, if on the quantum side we use polynomial-time distinguishers, but on the classical side we use distinguishers that are able to simulate quantum polynomial-time machines, then protocols that are classically secure remain secure when thought of as quantum computations.

\subsection{Setup assumptions and freely usable resources}\label{sec:set-up} %\anne{setup and free?...}

Cryptographers often prove results saying that a given functionality is impossible to realize in the \emph{plain} model but is possible with some \emph{setup}. For instance, in~\cite{CF01} they show that bit commitment (BC) is impossible in the plain UC-framework but it is possible assuming a common reference string (CRS)---a functionality that gives all parties the same string drawn from some fixed distribution. In our viewpoint, claims such as these can be interpreted in the categories we have already built: for instance, impossibility of commitments amounts to non-existence of a secure map $I\to BC$ that builds bit commitments out of a trivial resource $I$, and possibility of bit commitments given a common reference string amounts to the existence of a secure protocol $CRS\to BC$.

A related, but distinct matter is that sometimes cryptographers wish to make some (possibly shared) functionalities freely available to all parties without having to explicitly mention them being used as a resource. For instance, so far in our framework all communication between the honest parties has been mediated by the functionality $r$ that they start from. However, one might want to model situations where \eg pairwise communication between parties is freely available (as is standard in multi-party computation) and does not need to be provided explicitly by the functionality one starts from. Put more abstractly, one might wish to declare some set $\mathcal{X}$ of functionalities ``free'' and think of secure protocols that build $s$ from  $r$ and some functionalities from $\mathcal{X}$ just as maps $r\to s$, without having to explicitly keep track of how many copies of which $x\in \mathcal{X}$ was used. This is in fact something that happens quite often in resource theories even before any security conditions arise, as it could happen that the free processes $\CF$ are not quite expressive enough for the resource theory at hand. While one could try to define a larger category of free processes directly, it might be technically more convenient to obtain a larger class of free processes by allowing resource transformations to consume a resource from some class that is considered free. This can be achieved via a general construction on SMCs, a special case used in~\cite{fongetal:backprop} when constructing the category of learners. A special case also appears in the resource theory of contextuality as defined in~\cite{abramskyetal:comonadicview}, where one first defines deterministic free processes, and probabilistic (but classical) transformations $d\to e$ are then defined as transformations $d\otimes c\to e$ where $c$ is a non-contextual (and thus free) resource. This construction is discussed more generally in~\cite{Gavranovic:compositional,cruttwell2021categorical}, but we modify it slightly by allowing one to choose a class of objects as ``parameters'' instead of taking that class to consist of all objects: this modification is important for resource theories as it lets one can control which resources are made freely available.
\begin{proposition}\label{prop:paraconstruction}
Let $\C$ be a SMC and $\mathcal{X}$
a class of objects that contains $I$ and is closed under $\otimes$. Then there is a SMC whose objects are those of $\C$, and whose morphisms $A\to B$ are given by equivalence classes of morphisms $A\otimes X\to B$ in $\C$ with $X\in\mathcal{X}$, where $f\colon A\otimes X\to B$,$f'\colon A\otimes X'\to B$ are equivalent if there is an isomorphism $g\colon X\to X'$ such that $f=f'\circ(\id[A]\otimes g)$
\end{proposition}

\begin{proof}[Sketch] The composites $g\circ f$ and $g\otimes f$ are depicted by
\[
\begin{pic}
\node[morphism] (f) at (0,0) {$f$};
\setlength\minimummorphismwidth{6mm}
\node[morphism] (g) at (0.32,.9) {$g$};
\draw ([xshift=-2pt]f.south west) to +(0,-.4) node[left] {$A$};
\draw ([xshift=2pt]f.south east) to +(0,-.4) node[right] {$X$};
\draw (f) to ([xshift=-2pt]g.south west);
\draw ([xshift=2pt]g.south east) to +(0,-1.3) node[right] {$Y$};
\draw (g.north) to +(0,.35) node[right] {$C$};
\end{pic}
\qquad\qquad
\begin{pic}
\node[morphism] (f) at (0,0) {$f$};
\node[morphism] (g) at (.9,0) {$g$};
\draw ([xshift=-2pt]f.south west) to +(0,-.4) node[left] {$A$};
\draw ([xshift=2pt]f.south east) to[out=-90,in=90] +(0.52,-.4) node[below] {$X$};
\draw (f.north) to +(0,.3) node[left] {$B$};
\draw (g.north) to +(0,.3) node[right] {$D$};
\draw ([xshift=-2pt]g.south west) to[out=-90,in=90] +(-0.52,-.4) node[below] {$C$};
\draw ([xshift=2pt]g.south east) to +(0,-.4) node[right] {$Y$};
\end{pic}
\]
It is easy to show graphically that these are well-defined and that this results in a SMC. \end{proof}
Using Proposition~\ref{prop:paraconstruction} we can easily model protocols that have free access to some cryptographic functionalities: one just declares a class $\mathcal{X}$ of functionalities (\eg pairwise communication channels) that is closed under $\otimes$ to be free. In that case a protocol acting on $(A_{i=1}^n,r)$ can be depicted by
\[
\begin{pic}
\setlength\minimumstatewidth{9mm}
\setlength\morphismheight{3mm}
\node[state] (r) at (0,0) {$r$};
\node[state] (x) at (1.25,0) {$x$};
\node (a) at (0.6,.6) {$\ldots$};
\node (b) at (0,.1) {$\ldots$};
\node (c) at (1.25,.1) {$\ldots$};
\node[morphism,font=\tiny] (f) at (-0.04,.55) {$f_1$};
\node[morphism,font=\tiny] (g) at (1.29,.55) {$f_n$};
\draw ([xshift=-0pt]r.A) to ([xshift=-2pt]f.south west);
\draw ([xshift=-0pt]x.A) to [in=-90,out=90] ([xshift=2pt]f.south east);
\draw ([xshift=0pt]r.B) to [in=-90,out=90]  ([xshift=-2pt]g.south west);
\draw ([xshift=0pt]x.B) to ([xshift=2pt]g.south east);
\draw (f.north) to +(0,.25);
\draw (g.north) to +(0,.25);
\end{pic}
\]
where $x\in\mathcal{X}$ is a free resource.
\end{document}